請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/85251
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chung-Yang Huang) | |
dc.contributor.author | Ching-Zong Chang | en |
dc.contributor.author | 張靖宗 | zh_TW |
dc.date.accessioned | 2023-03-19T22:53:01Z | - |
dc.date.copyright | 2022-09-30 | |
dc.date.issued | 2022 | |
dc.date.submitted | 2022-09-27 | |
dc.identifier.citation | [1] L. Devroye, 'Random variate generation for unimodal and monotone densities,' Computing, vol. 32, no. 1, pp. 43–68, Mar. 1984. [2] J. Yuan, A. Aziz, C. Pixley, and K. Albin, 'Simplifying Boolean Constraint Solving for Random Simulation-Vector Generation,' IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 23, no. 3, pp. 412–420, Mar. 2004. [3] N. Kitchen and A. Kuehlmann, 'A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints,' in Computer Aided Verification. pp. 446–461, Springer. 2009. [4] S. M. Plaza, I. L. Markov, and V. Bertacco, 'Random stimulus generation using entropy and XOR constraints,' in the conference, Munich, Germany, Mar. 10–14, 2008. [5] Shujun Deng, Zhiqiu Kong, Jinian Bian, and Yanni Zhao, 'Self-adjusting constrained random stimulus generation using splitting evenness evaluation and XOR constraints,' in 2009 Asia and South Pacific Design Automation Conference (ASP-DAC), Yokohama, Japan, Jan. 19–22, 2009. [6] M. A. Iyer, 'Race a word-level atpg-based constraints solver system for smart random simulation,' in International Test Conference, 2003. ITC 2003., Washington, DC, USA. IEEE. Sep. 17, 2022. [7] B.-H. Wu, C.-J. Yang, and C.-Y. Huang, 'A High-Throughput and Arbitrary-Distribution Pattern Generator for the Constrained Random Verification,' IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 33, no. 1, pp. 139–152, Jan. 2014. [8] V. Bertacco, 'Distance-Guided Hybrid Verification with GUIDO,' in 2006 IEEE International High Level Design Validation and Test Workshop, Monterey, CA, USA, Nov. 8–10, 2006. [9] F. M. De Paula and A. J. Hu, 'An Effective Guidance Strategy for Abstraction-Guided Simulation,' in 2007 44th ACM/IEEE Design Automation Conference, San Diego, CA, USA, Jun. 4–8, 2007. [10] Y. Zhou, T. Wang, H. Li, T. Lv, and X. Li, 'Functional Test Generation for Hard-to-Reach States Using Path Constraint Solving,' IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 35, no. 6, pp. 999–1011, Jun. 2016. [11] I. C. S. D. A. S. Committee, IEEE standard for SystemVerilog--unified hardware design, specification, and verification language, 2nd ed. New York: Institute of Electrical and Electronics Engineers, 2010. [12] E. Clarke, 'Counterexample-guided abstraction refinement,' in 10th International Symposium on Temporal Representation and Reasoning and Fourth International Conference on Temporal Logic. TIME-ICTL 2003. [13] K. L. McMillan, 'Interpolation and SAT-Based Model Checking,' in Computer Aided Verification. Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 1–13, 2003. [14] N. Eén, A. Mishchenko, and R. Brayton, 'Efficient implementation of property directed reachability,' in Formal Methods in Computer-Aided Design (FMCAD) pp. 125-134, October, 2011. [15] 'Veripool.' Veripool · Veripool. https://www.veripool.org/verilator/ (accessed Sep. 17, 2022). [16] 'Yosys Open SYnthesis Suite.' YosysHQ. https://yosyshq.net/yosys/ (accessed Sep. 17, 2022). [17] Y. Shi, C. W. Ting, B.-H. Gwee, and Y. Ren, 'A highly efficient method for extracting FSMs from flattened gate-level netlist,' in 2010 IEEE International Symposium on Circuits and Systems - ISCAS 2010, Paris, France, May 30–Jun. 2, 2010. [18] R. De Maesschalck, D. Jouan-Rimbaud, and D. L. Massart, 'The Mahalanobis distance,' Chemometrics and Intelligent Laboratory Systems, vol. 50, no. 1, pp. 1–18, Jan. 2000. [19] 'GitHub - ZipCPU/zipcpu: A small, light weight, RISC CPU soft core.' GitHub. https://github.com/ZipCPU/zipcpu (accessed Sep. 17, 2022). | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/85251 | - |
dc.description.abstract | 隨著積體電路規模與複雜度的增長,功能驗證在晶片設計流程中的重要性日增。基於模擬的約束隨機驗證方法,因能有效處理複雜度指數成長的大規模晶片設計,而成為業界的主流驗證方式。但其追求高生成率與均勻分布的特性,使測試向量在策略性與目的性上都有所不足,模擬器只能在設計狀態空間中以隨機遊走的方式進行探索。本研究提出設計抽象化技術提供晶片設計與反例的宏觀全局結構模型,再結合精緻化技術來有系統性的補充與驗證目標有關的必要設計細節。據此指引生成器有目的性的生成測試向量。在大規模數位系統的實驗結果顯示,我們的方法在驗證安全屬性的能力、速度與給出的反例質量上都明顯優於原始方法。 | zh_TW |
dc.description.abstract | With the rapid growth in the scale and complexity of integrated circuits, functional verification has become increasingly important in the IC design flow. Simulation-based Constrained random methods can effectively handle the exponential growth of large-scale designs. Therefore, it has become the mainstream verification method in the industry. However, its high throughput and uniform distribution in probability make the generated patterns unplanned and meaningless. The simulator can only explore the design state space by random walk. This thesis proposes a design abstraction technique to provide an abstract model of the design and counterexamples, combined with refinement techniques to systematically supplement it with the necessary details related to the verification goals. This 'big picture' model guides the generator to produce more purposeful patterns. Experimental results on large-scale digital systems show that our method significantly outperforms the original approach in runtime, verification ability, and quality of counterexamples. | en |
dc.description.provenance | Made available in DSpace on 2023-03-19T22:53:01Z (GMT). No. of bitstreams: 1 U0001-2709202213364400.pdf: 22087207 bytes, checksum: 7b60c2aa42d8742a4bcfe51123269310 (MD5) Previous issue date: 2022 | en |
dc.description.tableofcontents | 誌謝 i 中文摘要 ii ABSTRACT iii CONTENTS iv LIST OF FIGURES vi LIST OF TABLES viii Chapter 1 Introduction 1 1.1 Motivation 1 1.2 Related Work 2 1.3 Contributions 4 1.4 Thesis Organization 5 Chapter 2 Background Knowledge 6 2.1 Functional Verification in IC Design Flow 6 2.2 Abstraction and Refinement 10 2.3 Formal-Based Verification 12 2.4 Simulation-Based Verification 14 Chapter 3 Overview of Constrained Random Pattern Generation 15 3.1 The Architecture of Our Framework 15 3.2 An Example for Challenge of Constrained Random Verification 17 Chapter 4 Feedback Modeling for Safety Property Violation 19 4.1 Terminology Definition 20 4.2 Feedback Model Definition 22 4.3 The Policy of Pattern Generation for the Shortest Counterexample 24 4.4 Issues of Large-Scale Design Modeling 25 Chapter 5 Model Abstraction for Large-Scale Designs 26 5.1 Abstraction on Design State Space 27 5.2 Abstraction on Transition Probability Matrix 29 5.3 Abstraction on Input Pattern Space 31 5.4 Abstraction on Counterexample 33 5.5 Approximation of Feedback Function 34 5.6 Issues of Abstract Counterexample Mismatch 36 Chapter 6 Refinement Process for Repairing of Abstraction Mismatch 37 6.1 Counterexample Refinement by Multi-cycle Expansion 39 6.2 The Exploration-exploitation Trade-off 41 6.3 Heuristic Caching Strategy for Accelerating Expansion 43 Chapter 7 Experiment 46 7.1 A Brief Overview of the Design Under Verification 46 7.2 The Details of Safety Properties 48 7.3 Experimental Results 51 Chapter 8 Conclusion 53 8.1 Summary 53 8.2 Further Work 54 REFERENCE 55 | |
dc.language.iso | en | |
dc.title | 運用設計自動抽象化技術增進限制隨機向量生成效能 | zh_TW |
dc.title | Improving Constrained Random Pattern Generation by Automatic Design Abstraction | en |
dc.type | Thesis | |
dc.date.schoolyear | 110-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 王柏堯(Bow-Yaw Wang),吳安宇(An-Yeu Wu) | |
dc.subject.keyword | 功能性測試,限制隨機驗證,抽象化與精細化, | zh_TW |
dc.subject.keyword | Functional Verification,Constrained Random Verification,Abstraction and Refinement, | en |
dc.relation.page | 56 | |
dc.identifier.doi | 10.6342/NTU202204156 | |
dc.rights.note | 同意授權(限校園內公開) | |
dc.date.accepted | 2022-09-28 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
dc.date.embargo-lift | 2022-09-30 | - |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
U0001-2709202213364400.pdf 授權僅限NTU校內IP使用(校園外請利用VPN校外連線服務) | 21.57 MB | Adobe PDF | 檢視/開啟 |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。