請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/52350
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chung-Yang (Ric) | |
dc.contributor.author | Hong-Syun Jiang | en |
dc.contributor.author | 江弘勛 | zh_TW |
dc.date.accessioned | 2021-06-15T16:12:31Z | - |
dc.date.available | 2015-08-20 | |
dc.date.copyright | 2015-08-20 | |
dc.date.issued | 2015 | |
dc.date.submitted | 2015-08-18 | |
dc.identifier.citation | [1] K.L. McMillan D.L. Dill L.J. Hwang J.R. Burch, E.M. Clarke. Symbolic model checking: 1020 states and beyond. Logic in Computer Science, pages 428 – 439, Jun 1990.
[2] N. Een and N.Sorensson. Minisat - a sat solver with conflict-clause minimization. In SAT, 2005. [3] E. Clarke A. Biere, A.Cimatti and Y. Zhu. Symbolic model checking without bdds. Tool and Algorithms fot the Construction and Analysis of Systems, pages 193–207, 1999. [4] E.M. Clarke M. Fujita Y. Zhu A. Biere, A. Cimatti. Symbolic model checking using sat procedures instead of bdds. ACM/IEEE Design Automation Conference, 1999. [5] K.L. McMillan. Interpolation and sat-based model checking. Computer Aid Verifi- cation, page 113, 2003. [6] A.R.Bradley F., Somenzi. Ic3: Where monolithic and incremental meet. In FMCAD, 2011. [7] R. Brayton N. Een, A. Mishchenko. Efficient implementation of property directed reachability. In FMCAD, 2011. [8] Berkeley Logic Synthesis and Verification Group. Abc: A system for sequential synthesis and verification. http://www.eecs.berkeley.edu/alanmi/abc. [9] C.-Y. Wu and C.-Y. R. Huang. V3: An extensible framework for hardware verifica- tion. http://dvlab.ee.ntu.edu.tw/ publication/V3/. 48[10] E.M. CLARKE M.C. BROWNE and O. GRUMBERG. Characterizing finite kripke structures in propositional temporal logic. Theoretical Computer Science, 1988. [11] A. P. Sistla E. M. Clarke, E. A. Emerson. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Pro- gramming Languages and Systems (TOPLAS), 8(2):244–263, April 1986. [12] Hardware model checking competition http://fmv.jku.at/hwmcc/. [13] AT&T Research and Lucent Bell Labs. Graphviz - graph visualization tools. [14] Chih-Chung Chang and Chih-Jen Lin. LIBSVM: A library for support vector ma- chines. ACM Transactions on Intelligent Systems and Technology, 2:27:1–27:27, 2011. Software available at http://www.csie.ntu.edu.tw/~cjlin/ libsvm. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/52350 | - |
dc.description.abstract | 隨著數位電路規模快速成長,對於模式驗證效率的要求也越來越高,近年來各種針對模式驗證的演算法如雨後春筍般出現,其中最具代表性的就是2011年由Aaron Bradley與Niclas Een發表的性質導向可達度技術,直到現在該技術依然是解決大多數模式驗證問題最有效的方法,然而隨著電路越趨複雜規模越來越龐大,許多電路驗證問題仍然無法在可接受的時間內解決,因此本篇論文針對性質導向可達度技術進行分析,並提出三個不同的變形,再藉由對於解題時產生的模塊進行分析決定該使用何種變形,企圖提升性質導向可達度技術之效率,解決更多模式驗證問題. | zh_TW |
dc.description.abstract | Sequential verification is an important practical problem in these years. But it is hard to solved, both model checking and equivalence checking. There are many different techniques solving this problem such as BMC, ITP, and PDR. In all these different techniques, the recently developed PDR works best. Nevertheless, restricted by its NP complexity, many sequential verification problems remain unsolved. In this thesis we focus on how PDR work on these problems, and construct a cube analysis method try to figure out the bottleneck of PDR. Through the analysis we generate three different algorithms to help PDR get better performance. At the end we integrate all three methods and the original PDR in order to seek complete improvement on hardware model checking problem. | en |
dc.description.provenance | Made available in DSpace on 2021-06-15T16:12:31Z (GMT). No. of bitstreams: 1 ntu-104-R02943090-1.pdf: 2253048 bytes, checksum: a3fc2e1a81b2ed02b07f4da8abd60c6e (MD5) Previous issue date: 2015 | en |
dc.description.tableofcontents | 口試委員審定書 i
致謝 ii 中文摘要 iii Abstract iv Contents v List of Figures viii List of Tables x 1. Introduction 1 1.1 Motivation 2 1.2 Contribution of this Thesis 2 1.3 Organization of this Thesis 4 2.Preliminaries 5 2.1 Propositional Satisfiability 5 2.2 Model Checking Problem 5 2.2.1 Definition of Model Checking Problem 6 2.2.2 Safety Checking Problem 6 2.3 Property Directed Reachability 7 2.4 Overview of Recursive Block Phase on PDR 8 2.5 Recursive Block Diagram 11 3.Cube Analysis Algorithm 14 3.1 Method 1 : Enlarge Cubes 15 3.1.1 Motivation 15 3.1.2 Enlarge Cubes Algorithm 16 3.1.3 Case Study 17 3.1.4 Discussion 21 3.2 Method 2 : Select Cubes 23 3.2.1 Motivation 23 3.2.2 Overview of Select Cube Method 24 3.2.3 Implementtation Issue of Select Cubes Method 27 3.2.4 Discussion 28 3.3 Metthod 3 : Multiple Cubes 29 3.3.1 Motivation 29 3.3.2 Algorithm and Discussion 29 4. Prediction 31 4.1 Integrate All Method Together 31 4.1.1 Motivation 31 4.1.2 Directly Mix 31 4.1.3 Multiple Core 32 4.1.4 Prediction 32 4.2 Prediction Models 33 4.2.1 Single Prediction with Manually Scoring 33 4.2.2 Single Prediction with Support Vector Machine 34 4.2.3 Multiple Prediction with Support Vector Machine 35 5. Experiment Results 36 5.1 Comparison of Cube Analysis Methods 36 5.2 Comparison on Prediction Model 43 5.2.1 Manually Scoring Model 43 5.2.2 Single Prediction Model with SVM engine 44 5.2.3 Multiple Prediction Model with SVM engine 45 6. Conclusion and Future Work 46 Bibliography 48 | |
dc.language.iso | en | |
dc.title | 應用模塊分析提升性質導向可達度技術 | zh_TW |
dc.title | Enhancing Property Directed Reachability Technique through Cube Analysis | en |
dc.type | Thesis | |
dc.date.schoolyear | 103-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 江介宏(Jie-Hong Roland Jiang),王柏堯(Bow-Yaw Wang),吳政穎(Cheng-Yin Wu) | |
dc.subject.keyword | 模式驗證,性質導向可達度,模塊分析,循序電路驗證, | zh_TW |
dc.subject.keyword | Model Checking,Safety Property Checking,Property Directed Reachability,Sequential Verification, | en |
dc.relation.page | 49 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2015-08-18 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-104-1.pdf 目前未授權公開取用 | 2.2 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。