請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/10432
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chung-Yang (Ric) | |
dc.contributor.author | Cheng-Yin Wu | en |
dc.contributor.author | 吳政穎 | zh_TW |
dc.date.accessioned | 2021-05-20T21:29:05Z | - |
dc.date.available | 2010-08-21 | |
dc.date.available | 2021-05-20T21:29:05Z | - |
dc.date.copyright | 2010-08-21 | |
dc.date.issued | 2010 | |
dc.date.submitted | 2010-08-18 | |
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 J. Hwang. “Symbolic model checking: 10^20 states and beyond”. Information and Computation, 98(2): pages 142–170, 1992. [3] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. [4] A. Biere, A. Cimatti, E. Clarke and Y. Zhu, “Symbolic Model Checking without BDDs”. In Proc. 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, vol. 1579 of LNCS, pp. 193 – 207, 1999 [5] M. Sheeran, S. Singh, G. St_almarck. “Checking safety properties using induction and a SAT-solver”. FMCAD 2000 [6] 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. [7] 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 [8] Clarke, E. M., Grumberg, O., and Long, D. E., “Model Checking and Abstraction”. ACM Trans. Prog. Lang. Syst. (TOPLAS) 16, 5, 1512–1542, Sept 1994 [9] K.L. McMillan, “Interpolation and SAT-based model checking”. In Proc of CAV ‘03, pp. 1-13, LNCS 2725, Springer, 2003 [10] H. Jain, D. Kroening, N. Sharygina, and E. M. Clarke, “Word level predicate abstraction and refinement for verifying RTL verilog”. In Proceedings of the 42nd Annual Conference on Design Automation, pages 445–450, June 2005 [11] IEEE Standard Verilog Hardware Description Language. IEEE Standard 1364-2001. Institute of Electrical and Electronics Engineers, 2001. [12] IEEE Standard Open SystemC Language Reference Manual. IEEE Standard 1666-2005. Institute of Electrical and Electronics Engineers, 2005. [13] R. E. Bryant, “Graph-based algorithms for boolean function manipulation”. IEEE Trans. on Comp., 35(8):677-691, 1986 [14] S. A. Cook, “The Complexity of Theorem-Proving Procedures”. In Proc. Third Annual ACM Symposium on Theory of Computing, pp. 151 – 158, 1971. [15] A. Biere, “PicoSAT Essentials”. In Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, pp. 75 – 97, 2008 [16] W. Craig. “Linear reasoning: A new form of the Herbrand-Gentzen theorem”. J. Symbolic Logic, 22(3):250–268, 1957 [17] P. Pudlak., “Lower bounds for resolution and cutting plane proofs and monotone computations.” J. Symbolic Logic, 62(2):981–998, June 1997 [18] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and Veith H., “Counterexample-guided abstraction refinement”. In CAV, pages 154–169. Springer-Verlag, 2000 [19] C.-F. Huang, “Quick RTL Synthesis for Design Analysis and Verification”. Master’s thesis, National Taiwan University, Taipei, Taiwan, 2006. [20] “Berkeley Logic Interchange Format (BLIF)”. University of California. Berkeley. July 28, 1992 [21] Chi-Wen Chang, “High-Level Design Intent Extraction for Intelligent Verification”, Graduate Institute of Electronics Engineering College of Electrical Engineering & Computer Science, National Taiwan University Master Thesis, June 2007 [22] Jhen-Cheng Ye, “Improving Safety Property Checking by High-Level Design Information”, Graduate Institute of Electronics Engineering College of Electrical Engineering & Computer Science, National Taiwan University Master Thesis, June 2009 [23] G. Tseitin. “On the complexity of derivation in propositional calculus”. Studies in Constr. Math. and Math. Logic, 1968 [24] ABC: A System for Sequential Synthesis and Verification, http://www.eecs.berkeley.edu/~alanmi/abc/ [25] OpenCores, http://opencores.org/ | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/10432 | - |
dc.description.abstract | 在現今的超大規模集成電路驗證問題上,特別是針對正確表達設計者意圖的屬性檢定,已經面臨了極大複雜度的議題。安全性屬性檢定是其中一個最重要的問題,是為了確保硬體系統將永遠不會走入一個設計者原先意想不到的狀態。然而在傳統上我們會在邏輯階層的布林電路上做屬性檢定,但缺點是此階層所擁有的訊息中已經失去了設計者原先的意圖。因此我們認為直接在高等抽象階層的電路上做安全性屬性檢定將會更有效率。
在這篇論文中,我們將提出一個完全以可滿足性為根基的安全性屬性檢定演算法。此演算法將直接作用於位元向量階層的暫存器轉移階層設計與屬性。我們為了更有效率的解決問題而採用了根基於抽象與精細化的技術。實驗結果已顯示出我們的方法在處理困難的屬性問題上,不論在執行時間或收斂的能力上都能夠有非常好的表現與改善。 | zh_TW |
dc.description.abstract | Verification on modern VLSI designs has encountered a tremendous challenge for large design complexity issue, especially for verifying expected behavior from designer’s intent. Safety property checking is one of the most important problems to ensure that the hardware system will never fall into a state that is unexpected by designers. However, traditional assertion checking is conducted on gate-level Boolean circuits. The drawback is that the designer’s original intent is lost in this level. Therefore, it will be more efficient to perform safety property checking directly on high-level design abstraction.
In this thesis, we proposed a purely SAT-based safety property checking algorithm in dealing with word-level RTL designs and properties. Our approach is based on abstraction and refinement techniques to solve the problem more efficiently. Experimental results have shown that our approach has great performance improvement in runtime and convergence ability in proving difficult properties. | en |
dc.description.provenance | Made available in DSpace on 2021-05-20T21:29:05Z (GMT). No. of bitstreams: 1 ntu-99-R97943067-1.pdf: 4382947 bytes, checksum: 2eff5e22ec4f7a500f15f344093f1a09 (MD5) Previous issue date: 2010 | en |
dc.description.tableofcontents | 摘要 ii
Abstract iii Table of Contents iv List of Figures vi List of Tables viii Chapter 1 Introduction 1 Chapter 2 Preliminaries 4 2.1 Model Checking 4 2.1.1 Definition of Model Checking 4 2.1.2 Safety Property Checking 5 2.2 Related Works on Model Checking 6 2.2.1 Symbolic Model Checking 6 2.2.2 Bounded Model Checking 7 2.2.3 K-induction 9 2.2.4 Interpolation and SAT-based Model Checking 11 2.2.5 Counter-Example Guided Abstraction and Refinement 13 Chapter 3 An Overview of our Framework 15 3.1 Word-level QuteRTL Framework 15 3.2 The Overall Abstraction and Refinement Algorithm 16 3.2.1 Inspiration and Perspective in Solving the Problem 21 3.2.2 Comparison to Interpolation-based Approach in Flows 23 3.3 Preceding Works before Abstraction and Refinement 24 3.3.1 Construction of PUVGraph 25 3.3.2 Building Time Frame Expansion Circuit to SAT Solvers 27 3.3.3 Representation and Definition of States 30 3.3.4 Encoding of States in BMC_Solver 31 3.3.5 Encoding of States in Fix_Solver 32 Chapter 4 Word-level Abstraction and Refinement 34 4.1 Abstraction Phase 34 4.1.1 Inspection to High-level Abstraction 34 4.1.2 Cut Generation for Predicates 36 4.1.3 Concrete State and Abstract State 37 4.1.4 Algorithm in Abstraction Phase 39 4.1.5 Intelligent Guessing Algorithm 44 4.2 Refinement Phase 46 4.2.1 Check the Time for Refinement 46 4.2.2 Algorithm in Refinement Phase 47 4.3 Fixed-Point Check Phase 48 Chapter 5 Experimental Results 51 5.1 Test Environment 51 5.2 Results under Different Strategies 52 5.2.1 Comparison between Different Abstraction Strategies 52 5.2.2 Comparison between Different Refinement Strategies 56 5.3 Comparison with Berkeley ABC 58 Chapter 6 Conclusions and Future Work 64 Reference 65 | |
dc.language.iso | en | |
dc.title | 應用抽象與精細化技術增進RTL電路之安全性屬性檢定效能 | zh_TW |
dc.title | Improving Safety Property Checking on RTL Design with Abstraction and Refinement Techniques | en |
dc.type | Thesis | |
dc.date.schoolyear | 98-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 江介宏(Jie-Hong Roland Jiang),顏嘉志(Chia-Chih Yen) | |
dc.subject.keyword | 驗證,安全性屬性檢定,可滿足性,暫存器轉移階層,抽象與精細化, | zh_TW |
dc.subject.keyword | Verification,Safety Property Checking,Satisfiability,Register-Transfer-Level,RTL,Abstraction and Refinement, | en |
dc.relation.page | 67 | |
dc.rights.note | 同意授權(全球公開) | |
dc.date.accepted | 2010-08-19 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-99-1.pdf | 4.28 MB | Adobe PDF | 檢視/開啟 |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。