郭斯彥Kyo, Sy-Yen臺灣大學:電子工程學研究所陳奐彣Chen, Huan-WenHuan-WenChen2010-07-142018-07-102010-07-142018-07-102008U0001-2407200813073000http://ntur.lib.ntu.edu.tw//handle/246246/189283現今科技一日千里，IC設計的元件也越來越複雜。在現今業界裡，驗證已是重要的一環。在整個設計週期中，驗證約佔了三分之二強。但既使花在驗證上的時間越來越多，我們仍難以作完整性的功能涵蓋率驗證(Functional Coverage)驗證。 驗證的方法一般分為兩類。正規驗證(Formal approach)與模擬驗證(Simulation-based)。前者能對晶片做一完整的驗證，但在晶片設計越趨複雜的今天，這是無法被達成的。不論是商品上市的時間點，抑或是要完成它所需的幾近無限長的時間。而模擬驗證擁有快速、方便、易於使用等等的優點。也因此為工業界所廣為使用。但模擬驗證只能驗證到它模擬到的範圍，所以其涵蓋率就被限制住了。 本篇論文提出了一個使用Symbolic simulation的混合驗證方法。融合了正規驗證在涵蓋率上的優點，和模擬驗證的方便性。它的易於實作性讓工業界易於接受，增加其實用性，也是本方法最重要的優點。並在Alpha 上對此方法做了測試，證實其讓功能驗證變得更加完整與方便。Verification is an important part of the modern IC design, especially functional verification, which is responsible for 40% of the failure. There are two major verification methods that are being commonly used, simulation-based and formal approach. As the increasing complexity of modern design, the goal of proving functional correct is becoming more and more difficult to obtain. As the result, we introduce a scalable hybrid verification methodology to leverage the advantages of both simulation and formal approaches. The primary advantage of our method is that it can be implemented easily. We use a hybrid logic/symbolic simulator called Insight to transform the circuit into a SAT problem under restricted condition. And then, use an SAT solver to verify if it is satisfiable to prove its functional correct.口試委員會審定書 i 謝 ii要 iiibstract ivhapter 1 Introduction 1.1 Verification 1.2 Verification Methodology 2.2.1 Simulation-based verification 3.2.2 Formal verification 5.2.3 Formal verification 6.3 Our approach 7hapter 2 Background 8.1 Simulation-Based Verification 9.1.1 Directed test 9.1.2 Constrained-Random Simulation Testbench 10.2 Formal Verification 10.2.1 Satisfiability Problem 12.2.2 Bounded Model Checking 13.2.3 Symbolic Simulation 14.2.4 Equivalence Checking 16.3 Algorithm and technique 18.3.1 And-inverter graph 18.3.2 Improvements to Combinational Equivalence Checking 22.3.3 Self-consistency 25hapter 3 Methods 27.1 Our approach 27.2 Alpha Architecture 29.2.1 Data Format 30.2.2 Instruction Format 30.2.3 Instruction 31.2.4 Instruction Set Characteristics 33.3 Bugs Overview 34.4 ABC Overview 36hapter 4 Implementation of the Scalable Formal Verificatio 41.1 Insight 42.1.1 List Functions 43.1.2 Symbolic simulation 46.2 SAT Problem 47hapter 5 Experimental Result and Discussion 49.1 Sequential Equivalence Checking (SEC) Benchmark 49hapter 6 Conclusion and Future Work 53.1 Conclusion 53.2 Future Work 54eference 55136 bytestext/htmlen-US微處理器驗證混合方法符號模擬正規功能驗證晶片設計Alphamicroprocessorformalsimulation-basedverificationhybrid methodologyfunctional verificationthesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/189283/1/index.html