黃鐘揚Huang, Chung-Yang (Ric)臺灣大學:電子工程學研究所饒瑞晞Rau, Ruey-ShiRuey-ShiRau2010-07-142018-07-102010-07-142018-07-102009U0001-2506200919335200http://ntur.lib.ntu.edu.tw//handle/246246/189229現代的數位硬體設計多半從暫存器轉移階層開始描述，再經由一連串的自動化操作直到實體電路設計完成。而由於早期發現設計錯誤所需的成本遠較後期發現為低廉，因此暫存器轉移階層的驗證至關重要。滿足性解法器為正規驗證中重要的核心引擎。為此，本論文提出一專為暫存器轉移階層驗證而設計之可滿足性解法器。此解法器基於Davis-Putnam-Logemann-Loveland演算法，配合位元向量階層的電路描述、各種位元向量邏輯閘的蘊涵關係、以及專為各種位元向量邏輯閘特別設計的矛盾分析。相較於其他的解法器，我們的解法器不僅保留了電路結構的相關資訊，更由於我們並未將位元向量階層的邏輯閘展開為單一位元邏輯閘的集合，更多暫存器轉移階層的資訊因而得以被保留，且可應用於解題過程之中。實驗結果顯示，我們的解法器效能足以和當今一流的解法器相匹敵。Modern digital hardware design begins from register-transfer-level (RTL) description. Then, the RTL description passes through a series of design automation procedures until the physical layout is completed. Since the cost of design errors is much lower if they are found in earlier design stages, the verification on RTL is very important.he satisfiability solver is one of the essential core engines for formal verification. Therefore, this thesis proposed a word-level satisfiability solver for RTL design verification, QuteWSat. QuteWSat combines David-Putnam-Logemann-Loveland algorithm, word-level circuit description, implication procedures and conflict analysis procedures for each type of word-level logic gates. Compared with other satisfiability solvers, QuteWSat preserves the structural information about the circuit, and since it does not expand word-level logic gates into bit-level logic gates, some RTL information can be preserved and utilized in the solving process. The experimental results show that the performance of QuteWSat is comparable to that of a state-of-the-art solver.口試委員審定書 i謝 ii要 iiibstract ivable of Contents vist of Figures viiiist of Tables xhapter 1 Introduction 1hapter 2 Preliminaries 3.1 Boolean Satisfiability Solving Techniques 3.1.1 Davis-Putnam-Logemann-Loveland (DPLL) Algorithm 3.1.2 Boolean Constraint Propagation 4.1.3 Conflict Analysis 7.1.4 Decision Heuristic 10.2 Word-Level Satisfiability Solving Techniques 11.2.1 Bit-Blasting 11.2.2 Linear Programming Approaches 12.2.3 Word-Level Automatic Test Pattern Generation (ATPG) and DPLL 13.2.4 Abstraction and Refinement 15hapter 3 An Overview of QuteWSat 19.1 Problem Modeling in QuteWSat 19.2 The Overall Algorithm 22.3 Implementation 24hapter 4 Constraint Propagation 29.1 Event Scheduling 29.2 Constraint Propagation on Different Gate Types 29.2.1 Boolean Gates 30.2.2 Multiplexers 30.2.3 Comparators 31.2.4 Arithmetic Gates 34.2.5 Shift Gates 36.2.6 Bus Gates and Variables 37.3 Constraint Propagation on Learned Clauses 37hapter 5 Conflict Analysis 38.1 Antecedent Recording 38.2 Learned Clause Generation 38.3 Extracting the Implication Sources for Different Gate Types 41.3.1 Boolean Gates 42.3.2 Multiplexers 42.3.3 Comparators 43.3.4 Arithmetic Gates 44.3.5 Shift Gates 45.3.6 Bus Gates 46hapter 6 Experimental Results 48.1 BTOR Format 48.2 SMT-LIB Benchmark Suite 51.3 Comparison with Yices 51.4 Profiling 53hapter 7 Conclusions and Future Work 56eference 571116389 bytesapplication/pdfen-US驗證可滿足性問題可滿足性解法器暫存器轉移階層DPLLVerificationSatisfiability ProblemSatisfiability SolverRegister-Transfer-LevelRTL[SDGs]SDG16thesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/189229/1/ntu-98-R96943067-1.pdf