請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/62162
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chung-Yang Huang) | |
dc.contributor.author | Yu-Yun Dai | en |
dc.contributor.author | 戴伃芸 | zh_TW |
dc.date.accessioned | 2021-06-16T13:31:13Z | - |
dc.date.available | 2013-07-26 | |
dc.date.copyright | 2013-07-26 | |
dc.date.issued | 2013 | |
dc.date.submitted | 2013-07-22 | |
dc.identifier.citation | [1] S. A. Cook, “The Complexity of Theorem-Proving Procedures”. In Proc. Third Annual ACM Symposium on Theory of Computing, pp. 151 – 158, 1971.
[2] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang and S. Malik, “Chaff: Engineering an Efficient SAT Solver”. In Proc. Design Automation Conference, pp. 530 – 535, 2001. [3] N. Een and N. Sorensson, “An Extensible SAT-Solver”. In Proc. Theory and Applications of Satisfiability Testing, vol. 2919 of LNCS, pp. 502 – 518, 2004. [4] Mate Soos, “Enhanced Gaussian Elimination in DPLL-based SAT Solvers”. In Pragmatics of SAT Workshop, 2010. [5] IEEE Standard Verilog Hardware Description Language. IEEE Standard 1364-2001. Institute of Electrical and Electronics Engineers, 2001. [6] IEEE Standard VHDL Language Reference Manual. IEEE Standard 1076-2002. Institute of Electrical and Electronics Engineers, 2002. [7] H.H. Yeh, C.Y. Wu, and C.Y. (Ric) Huang. “QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification”. In Proc. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2012. [8] S. K. Lahiri, S. A. Seshia, and R. E. Bryant. “Modeling and Verification of Out-of-order Microprocessors using UCLID”. In Proc. Formal Methods in Computer-Aided Design, vol. 2919 of LNCS, pp. 142-159, 2002. [9] R. Brummayer and A. Biere, “Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays”. In Proc. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 5505 of LNCS, pp. 174 – 177, 2009. [10] R. Bruttomesso, A. Cimatti, A. Franzen, A. Griggio, and R. Sebastiani, “The MathSAT 4 SMT Solver”. In Proc. Computer-Aided Verification, vol. 5123 of LNCS, 2008. [11] L. de Moura and N. Bjorner, “Z3: An Efficient SMT Solver”. In Proc. Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 4963 of LNCS, pp. 337–340, 2008. [12] M. Davis, G. Logemann and D. Loveland, “A Machine Program for Theorem-Proving”. In Communications of the ACM, vol. 5, pp. 394 – 397, 1962. [13] J. P. Marques Silva and K. A. Sakallah, “GRASP – A New Search Algorithm for Satisfiability”. In Proc. International Conference on Computer-Aided Design, pp. 220 – 227, 1996. [14] C. Barrett, A. Stump and C. Tinelli, “The Satisfiability Modulo Theories Library (SMT-LIB)”. Available at http://www.smt-lib.org/ , 2010. [15] R. Brummayer, A. Biere, F. Lonsing, “BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking”. In Proc. Workshop on Bit-Precise Reasoning, 2008. [16] B. Dutertre and L. de Moura, “The YICES SMT Solver”. Available at http://yices.csl.sri.com/tool-paper.pdf , 2006. [17] “SMT-COMP ’12”. http://smtcomp.sourceforge.net/2012/ , 2012. [18] R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady, “Deciding Bit-Vector Arithmetic with Abstraction”. In Proc. Tools and Algorithms for the Construction and Analysis of Systems, vol. 4424 of LNCS, pp. 358 – 372, 2007. [19] H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras and C. Tinelli, “DPLL(T): Fast Decision Procedures”. In Proc. Computer-Aided Verification, 2004. [20] V. Ganesh and D. L. Dill, “A Decision Procedure for Bit-Vectors and Arrays”. In Proc. Computer Aided Verification, 2007. [21] C.-Y. Huang and K.-T. Cheng, “Using Word-Level ATPG and Modular Arithmetic Constraint-Solving Techniques for Assertion Property Checking”. In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 20, pp. 381 – 391, 2001. [22] D. R. Cok, “The SMT-LIBv2 Language and Tools: A Tutorial”. Available at http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf , 2013. [23] N. Een and N. Sorensson, “minisat-2.2.0.tar.gz”. Available at http://minisat.se/MiniSat.html, 2008. [24] “The GNU Multiple Precision Arithmetic Library”. Available at http://gmplib.org/, 2013. [25] “SMT-COMP ’08”. http://www.smtcomp.org/2008/, 2008. [26] “MathSAT Version 5.2.6”. Available at http://mathsat.fbk.eu/, 2013. [27] “Z3 4.1.2”. Available at http://z3.codeplex.com/, 2012 [28] C. M. Wintersteiger, Y. Hamadi, and L. de Moura, “Efficiently solving quantified bit-vector formulas”. In Proc. International Conference on Formal Methods in Computer-Aided Design, 2010. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/62162 | - |
dc.description.abstract | 作為當代正規驗證的核心引擎,布林階層的可滿足性解法器已有長足的發展。然而,為了在維持高階資訊下驗證暫存器轉移階層的設計,專門針對位元向量邏輯運算的高效率詞級可滿足性解法器有其發展的必要性。
因此,本論文針對位元向量邏輯運算的問題提出了一套詞級可滿足性解法器的演算法及其實作方法。此解法器積極地整合兩個不同的解法器:其一專門處理布林階層的滿足性問題,另一個則針對線性算術部分的問題。其中,一個原創的純粹詞級解法器被實作來處理線性算術限制,並同時處理等式與不等式。相較於其他的解法器,本論文提出的解法器能以處理線性限制的方式來處理算術運算元,而不是將其展開為單一位元邏輯閘的組合。實驗結果顯示,本論文所提出的解法器設計和實作方法能夠與現今一流的解法器有相近的效能,並能更有效的處理包含大量算術運算元的問題。 | zh_TW |
dc.description.abstract | As the core engines for formal verification, Boolean satisfiability solvers have been developed very well. However, to verify register-transfer-level designs without dismissing high level information, efficient word-level satisfiability solvers, which process logic operations over bit-vectors, are desired.
Therefore, this thesis proposed a word-level satisfiability solver, MeowSAT, for quantifier-free logics over bit-vectors, including its algorithms and implementations. MeowSAT performs lazy approach with eager integrations between two solvers, which are responsible for pure Boolean and linear arithmetic instances respectively. Indeed, an in-house pure word-level solver is implemented to process linear integer arithmetic equality and inequality constraints. Compared with other word-level satisfiability solvers, MeowSAT manipulates arithmetic operations with the constraint solver, not by fully expanding into Boolean logic gates. The experimental results show that the performance of MeowSAT is comparable to that of state-of-the art solvers, especially for those cases with high portion of arithmetic operators. | en |
dc.description.provenance | Made available in DSpace on 2021-06-16T13:31:13Z (GMT). No. of bitstreams: 1 ntu-102-R00943084-1.pdf: 870568 bytes, checksum: cc7e0070b2386e187c74b0931c6d9b71 (MD5) Previous issue date: 2013 | en |
dc.description.tableofcontents | 口試委員會審定書 #
誌謝 i 中文摘要 ii ABSTRACT iii CONTENTS iv LIST OF FIGURES vii LIST OF TABLES viii Chapter 1 Introduction 1 Chapter 2 Preliminary 3 2.1 Boolean Satisfiability Solving Techniques 3 2.1.1 Davis-Putnam-Logemann-LoveLand (DPLL) Algorithm 3 2.1.2 Boolean Constraint Propagation 5 2.1.3 Conflict Analysis 6 2.2 Word-Level Satisfiability Problems 8 2.2.1 Satisfiability Modulo Theories 9 2.2.2 QF-BV problems 10 2.3 Word-Level Satisfiability Solving Techniques 11 2.3.1 Eager Approach 11 2.3.2 Lazy Approach 13 Chapter 3 An Overview of MeowSAT 16 3.1 Problem Modeling 16 3.2 The Program Structure 18 3.3 The Overall Solving Procedure 20 3.4 Implementations for Gates 22 3.4.1 General Data Structure of Gates 23 3.4.2 Arithmetic Gates 24 3.4.3 Cross-domain gates 25 Chapter 4 Theories and Implementations for Pure Word-Level domain 28 4.1 Problem Instances and Data Structure 28 4.1.1 Class wordConstraint 28 4.1.2 Class wordClause 30 4.2 Operations for A Single Word-level Constraint 31 4.2.1 Simplification of a Word-level Constraint 31 4.2.2 Validation of a Word-level Constraints 33 4.3 Composition of Two Word-level Constraints 33 4.3.1 Steps for Word-level Composition 34 4.3.2 Relationships between Two Word-level Constraints 36 4.4 Pure Word-Level Solving Process 39 4.4.1 Overall Flow of Pure Word-level Solving 39 4.4.2 Pure Word-level Propagation 41 4.4.3 Word-level Conflict Analysis 46 4.4.4 Pure Word-level Assignment and Refinement 49 Chapter 5 Cross-domain Propagation and Conflict Analysis 51 5.1 Class solverManager 51 5.2 Overall Solving Flow in solverManager 52 5.3 Cross-domain Propagations 54 5.3.1 Boolean to Word-level Implication 54 5.3.2 Word-level to Boolean Implications 55 5.4 Conflict Analysis between Solvers 56 Chapter 6 Experimental Results 59 6.1 Experimental Settings and Benchmark Suites 59 6.2 Comparisons with Other Solvers 60 6.3 Case Studies 64 6.4 Strategy for Choosing Suitable Solvers 69 Chapter 7 Conclusion and Future Works 72 REFERENCE 74 | |
dc.language.iso | en | |
dc.title | MeowSAT: 基於多理論積極整合技術之詞級可滿足性解法器 | zh_TW |
dc.title | MeowSAT: A Word-Level Satisfiability Solver Based on Eager Integration of Theories | en |
dc.type | Thesis | |
dc.date.schoolyear | 101-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 江介宏(Jie-Hong Jiang),李建模(Chien-Mo Li),顏嘉志(Chia-Chih Yen) | |
dc.subject.keyword | 正規驗證,可滿足性問題,可滿足性模理論,詞級可滿足性解法器,線性整數算術, | zh_TW |
dc.subject.keyword | Formal Verification,Satisfiability Problem,Satisfiability Modulo Theories,Word-level Satisfiability Solvers,Linear Integer Arithmetic, | en |
dc.relation.page | 76 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2013-07-22 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-102-1.pdf 目前未授權公開取用 | 850.16 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。