黃鐘揚臺灣大學:電子工程學研究所葉鎮丞Ye, Jhen-ChengJhen-ChengYe2010-07-142018-07-102010-07-142018-07-102009U0001-2807200916570000http://ntur.lib.ntu.edu.tw//handle/246246/189230安全性屬性檢定在設計驗證之中是相當重要的技術。這項技術確保預期設計的正確性，或者當設計中的安全性屬性被違反時，能夠提供反例以供設計者偵錯。 在過去的研究當中，安全性屬性檢定在可滿足性解法器(SAT solver)的應用下解地不錯。由於要使用可滿足性解法器，問題本身會被翻譯至位元階層的邏輯式子，以便使用位元階層的邏輯操作如：化簡合取範式(CNF)和抽象並完善技術。但是這問題原本就來自暫存器轉移階層(RTL)設計。在暫存器轉移設計階層中，有許多高階設計資訊可能對安全性屬性檢定有幫助，例如有限狀態機(FSM)和字級表示式。在這篇論文中，字級表示式用來化簡邏輯表示式，從有限狀態機的資訊中抽取路徑限制用來幫助可滿足性解法器。我們的實驗顯現出我們的結果與另一個優秀的安全性檢定器ABC相當接近。部分測資在路徑限制的幫助下甚至能贏過ABC。因此高階設計資訊的確在安全性屬性檢定效能上有很好的提升效果。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.口試委員會審定書 #謝 i文摘要 iiBSTRACT iiiONTENTS ivIST OF FIGURES viiIST OF TABLES viiihapter 1 Introduction 1.1 Related Work 2.2 Research Contributions 6.3 Organization of this Thesis 7hapter 2 Preliminaries 8.1 Model checking 8.2 Safety Property 9.3 Bounded Model Checking 9.4 K-Induction on Bounded Model Checking 11.5 Converting Circuit to CNF 12.6 Bounded Model Checking on Sequential Circuits 13.7 High Level Design Intent - Finite State Machine 15.8 Local Finite State Machine 17.9 Product Machine of Multiple Local FSMs 18hapter 3 Proposed Algorithms for Safety Property Checking 20.1 Our Framework and Overall Flow 20.1.1 Implementation on QuteRTL 20.1.2 SAT Solver Engine: MiniSAT 21.1.3 Flow of our Algorithm 22.2 Model Construction for the Safety Property Checking 24.2.1 Construction for the Induction Step Model 25.2.2 Construction of the Base-Case Model 26.2.3 Translation of Word Level Gates to CNF Formulae 27.3 Product Machine Construction 29.4 Safety Property Checking with Incremental SAT 31.5 CNF Model Reduction by the Good Clause Generation Order 32.6 CNF Model Reduction by Word-Level Netlist Information 34.7 Extracting Path Constraints of the Abstract Product Machine to Guide the SAT Decision Procedure 38hapter 4 Experimental Results 40.1 Experimental Results of Incremental SAT 40.2 Experimental Results of CNF Clause Generation Order 41.2.1 CNF Clause generation in DFS order 41.2.2 Const-Node-First Strategy 41.3 Experimental Results of Using Super Mux 43.4 Experimental Results of Mux Select Signal Bumping 44.5 Experimental Results on Initial Decision Order 45.6 Experiment – Path Constraint 46hapter 5 Conclusions 48EFERENCE 49472302 bytesapplication/pdfen-US安全性屬性檢定高階設計資訊字級表示式有限狀態機safety property checkinghigh level design informationword-level expressionFinite State Machine(FSM)thesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/189230/1/ntu-98-R96943069-1.pdf