請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/42444
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚 | |
dc.contributor.author | Jhen-Cheng Ye | en |
dc.contributor.author | 葉鎮丞 | zh_TW |
dc.date.accessioned | 2021-06-15T01:13:53Z | - |
dc.date.available | 2009-07-30 | |
dc.date.copyright | 2009-07-30 | |
dc.date.issued | 2009 | |
dc.date.submitted | 2009-07-29 | |
dc.identifier.citation | [1] Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled, “Model Checking,” The MIT Press,1999.
[2] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, “Symbolic model checking: 1020 states and beyond”. Information and Computation, vol.98 no.2, pp.142–170, 1992. [3] A. Biere, A. Cimatti, E.M. Clarke and Y. Zhu, “Symbolic Model Checking without BDDs”. In Proc. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'99, vol.1579 of LNCS, pp. 193-207, 1999. [4] M. Sheeran, S. Singh, G. St_almarck, “Checking safety properties using induction and a SAT-solver”. In Proc. the 3rd International Conference on Formal Methods in Computer-Aided Design , vol.1954 of LNCS, pp. 108-125, 2000 [5] K.L. McMillan, “Interpolation and SAT-based model checking”. In Proc. Computer Aided Verification, vol. 2725 of LNCS, pp. 1-13, 2003 [6] W. Craig, “Linear reasoning: A new form of the Herbrand-Gentzen theorem”. J. Symbolic Logic, 22(3):250–268, 1957. [7] P. Pudlak., “Lower bounds for resolution and cutting plane proofs and monotone computations”. J. Symbolic Logic, 62(2):981–998, June 1997 [8] ABC: A System for Sequential and Verification, http://www.eecs.berkeley.edu/~alanmi/abc/ [9] A. Mishchenko, S. Chatterjee, R. Jiang, R. Brayton, “FRAIGs: A unifying representation for logic synthesis and verification”. ERL Technical Report, EECS Dept., UC Berkeley, March 2005 [10] N. Een, A. Mishchenko, and N. Sorensson, “Applying logic synthesis for speeding up SAT”. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT2007), vol.4501 of LNCS, pp. 272-286, 2007 [11] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-guided abstraction refinement”. In Proc. of Computer Aided Verification, vol. 1855 of LNCS, pp. 154-169, 2000 [12] M.D. Nguyen, D. Stoffel, M. Wedler, and W. Kunz, “Transition-by-Transition FSM Traversal for Reachability Analysis in Bounded Model Checking”. In Proc. International Conference on Computer Aided Design, pp. 1068-1075, 2005. [13] 張啟文, “High-Level Design Intent Extraction for Intelligent Verification”. 國立台灣大學電子工程研究所碩士論文 [14] G. Tseitin, “On the complexity of derivation in propositional calculus”. Studies in Constr. Math. and Math. Logic, 1968. [15] 黃俊輔, “Quick RTL Synthesis for Design Analysis and Verification”. 國立台灣大學電機工程研究所碩士論文 [16] Niklas Een, Niklas Sorenssonm, “An Extensible SAT-solver”. In Proc. the 6th International Conference on Theory and Applications of Satisfiability Testing, vol. 2919 of LNCS, pp.333-336, 2004. http://minisat.se/ [17] Niklas Een, Niklas Sorenssonm. “Temporal Induction by Incremental SAT Solving”. In Proc. First International Workshop on Bounded Model Checking, vol. 89(4) of ENTCS, 2003. [18] Chi-An Wu, Ting-Hao Lin, Chih-Chun Lee and Chung-Yang (Ric) Huang, “QuteSAT: A Robust Circuit-based SAT Solver for Complex Circuit Structure”. In Proc. the Conference on Design, Automation and Test in Europe, pp. 1-6, 2007. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/42444 | - |
dc.description.abstract | 安全性屬性檢定在設計驗證之中是相當重要的技術。這項技術確保預期設計的正確性,或者當設計中的安全性屬性被違反時,能夠提供反例以供設計者偵錯。 在過去的研究當中,安全性屬性檢定在可滿足性解法器(SAT solver)的應用下解地不錯。由於要使用可滿足性解法器,問題本身會被翻譯至位元階層的邏輯式子,以便使用位元階層的邏輯操作如:化簡合取範式(CNF)和抽象並完善技術。但是這問題原本就來自暫存器轉移階層(RTL)設計。在暫存器轉移設計階層中,有許多高階設計資訊可能對安全性屬性檢定有幫助,例如有限狀態機(FSM)和字級表示式。在這篇論文中,字級表示式用來化簡邏輯表示式,從有限狀態機的資訊中抽取路徑限制用來幫助可滿足性解法器。我們的實驗顯現出我們的結果與另一個優秀的安全性檢定器ABC相當接近。部分測資在路徑限制的幫助下甚至能贏過ABC。因此高階設計資訊的確在安全性屬性檢定效能上有很好的提升效果。 | zh_TW |
dc.description.abstract | Safety property checking is an important technique in design verification. It ensures the correctness of the expected design behavior, or, when the property is falsified, provides a counter example for debugging. In recent years, the problem is solved well with the help of SAT solver. Due to the nature of SAT solver, the problem input is translated into a bit-level logic formula and focused on the operation of bit-level logic like CNF minimization and abstraction and refinement technique. However, the problem is originally described in the RTL design. The high level design information such as Finite State Machine (FSM) and word-level expression might be helpful for the safety property checking problem. In this thesis, the word-level expression is used to reduce the logic representation, and the information provided by FSM is used to guide the SAT solver by path constraint. Our experimental result showed that the performance is closed to one of the safety property checker ABC. The performance with path constraint even wins the ABC. Thus, the high level design information does have a good effect on safety property checking. | en |
dc.description.provenance | Made available in DSpace on 2021-06-15T01:13:53Z (GMT). No. of bitstreams: 1 ntu-98-R96943069-1.pdf: 472302 bytes, checksum: 4ff0fa068b3b0369f164e96f1b18ab8f (MD5) Previous issue date: 2009 | en |
dc.description.tableofcontents | 口試委員會審定書 #
誌謝 i 中文摘要 ii ABSTRACT iii CONTENTS iv LIST OF FIGURES vii LIST OF TABLES viii Chapter 1 Introduction 1 1.1 Related Work 2 1.2 Research Contributions 6 1.3 Organization of this Thesis 7 Chapter 2 Preliminaries 8 2.1 Model checking 8 2.2 Safety Property 9 2.3 Bounded Model Checking 9 2.4 K-Induction on Bounded Model Checking 11 2.5 Converting Circuit to CNF 12 2.6 Bounded Model Checking on Sequential Circuits 13 2.7 High Level Design Intent - Finite State Machine 15 2.8 Local Finite State Machine 17 2.9 Product Machine of Multiple Local FSMs 18 Chapter 3 Proposed Algorithms for Safety Property Checking 20 3.1 Our Framework and Overall Flow 20 3.1.1 Implementation on QuteRTL 20 3.1.2 SAT Solver Engine: MiniSAT 21 3.1.3 Flow of our Algorithm 22 3.2 Model Construction for the Safety Property Checking 24 3.2.1 Construction for the Induction Step Model 25 3.2.2 Construction of the Base-Case Model 26 3.2.3 Translation of Word Level Gates to CNF Formulae 27 3.3 Product Machine Construction 29 3.4 Safety Property Checking with Incremental SAT 31 3.5 CNF Model Reduction by the Good Clause Generation Order 32 3.6 CNF Model Reduction by Word-Level Netlist Information 34 3.7 Extracting Path Constraints of the Abstract Product Machine to Guide the SAT Decision Procedure 38 Chapter 4 Experimental Results 40 4.1 Experimental Results of Incremental SAT 40 4.2 Experimental Results of CNF Clause Generation Order 41 4.2.1 CNF Clause generation in DFS order 41 4.2.2 Const-Node-First Strategy 41 4.3 Experimental Results of Using Super Mux 43 4.4 Experimental Results of Mux Select Signal Bumping 44 4.5 Experimental Results on Initial Decision Order 45 4.6 Experiment – Path Constraint 46 Chapter 5 Conclusions 48 REFERENCE 49 | |
dc.language.iso | en | |
dc.title | 利用高階設計資訊以增進電路之安全性屬性檢定效能 | zh_TW |
dc.title | Improving Safety Property Checking by High-Level Design Information | en |
dc.type | Thesis | |
dc.date.schoolyear | 97-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 王信博,王柏堯 | |
dc.subject.keyword | 安全性屬性檢定,高階設計資訊,字級表示式,有限狀態機, | zh_TW |
dc.subject.keyword | safety property checking,high level design information,word-level expression,Finite State Machine(FSM), | en |
dc.relation.page | 51 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2009-07-29 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-98-1.pdf 目前未授權公開取用 | 461.23 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。