請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/67171完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 黃鐘揚(Chung-Yang (Ric) | |
| dc.contributor.author | Cheng-Han Yang | en |
| dc.contributor.author | 楊承翰 | zh_TW |
| dc.date.accessioned | 2021-06-17T01:22:09Z | - |
| dc.date.available | 2018-08-20 | |
| dc.date.copyright | 2017-08-20 | |
| dc.date.issued | 2017 | |
| dc.date.submitted | 2017-08-10 | |
| dc.identifier.citation | [1] K. L. McMillan, Symbolic model checking. Springer US, 1993.
[2] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: Engineering an Efficient SAT Solver. DAC, 2001. [3] M. Sheeran, S. Singh, and G. Stålmarck, Checking safety properties using induction and a SAT-solver. FMCAD, 2000. [4] M. Brain, S. Joshi, D. Kroening, and P. Schrammel, Safety verification and refutation by k-invariants and k-induction. SAS. LNCS, 2015. [5] K. L. McMillan, Interpolation and SAT-based model checking. International Conference on Computer Aided Verification, 2003. [6] A. R. Bradley, SAT-based model checking without unrolling. VMCAI, 2011. [7] Hardware Model Checking contest. http://fmv.jku.at/hwmcc15/. [8] N. Een, A. Mishchenko, and R. Brayton, Efficient Implementation of Property Directed Reachability. FMCAD, 2011. [9] R. Brayton and A. Mishchenko, ABC: An academic industrial-strength verification tool. International Conference on Computer Aided Verification, 2010. [10] C.-Y. Wu and C.-Y. R. Huang, “V3: An extensible framework for hardware verification.” https://github.com/chengyinwu/V3. [11] K. Fan, M.-J. Yang, and C.-Y. R. Huang, Automatic abstraction refinement of TR in PDR. Asia and South Pacific Design Automation Conference, 2016. [12] Y. Vizel and A. Gurfinkel, Interpolating property directed reachability. ICCAD, 2014. [13] A. Ivrii and A. Gurfinkel, Pushing to the top. FMCAD, 2015. [14] M.-J. Yang and C.-Y. R. Huang, Improving Property Directed Reachability with Temporal Decomsition. Master Thesis, National Taiwan University, 2016. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/67171 | - |
| dc.description.abstract | 性質導向可達性技術自從在2011年被發表之後，一直是最有效率的模型驗證演算法。不像其他的演算法往往只偏向於安全或不安全的案例其中一者，性質導向可達性技術對於兩者都能有不錯的效能。然而，仍然有些案例是難以被解決的，所以一直有對於如何改進性質導向可達性技術的研究。在這篇論文中，我們提出了兩種將有界模型驗證融合進性質導向可達性技術的方法，以及一種結合原本的性質導向可達性技術和以上兩種演算法的混合演算法。我們在V3的框架上實做了我們的演算法，並用硬體模型驗證競賽的案例進行測試。實驗結果指出我們的演算法可以在較短的時間內解出比原本的演算法還多的案例。 | zh_TW |
| dc.description.abstract | Property Directed Reachability (PDR) has been the most efficient model checking algorithm since its publication in 2011. Unlike other algorithms which often prefers either SAT cases (bug finders) or UNSAT cases (prover), PDR is well balanced that it can solve both categories efficiently. However, there are still some hard cases that PDR fails to solve, so researchers keep finding ways to improve PDR. In this thesis, we propose two modifications that integrate the idea of bounded model checking (BMC) into PDR, and a hybrid version that combines those two methods with original PDR. We implement the algorithms on V3 framework and test the performance using HWMCC benchmarks. Experiment shows that our algorithm can solve more cases than the original PDR algorithm with less average runtime. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-17T01:22:09Z (GMT). No. of bitstreams: 1 ntu-106-R05921058-1.pdf: 1093364 bytes, checksum: 2ac2ae7aeee29adf5a983dd551217091 (MD5) Previous issue date: 2017 | en |
| dc.description.tableofcontents | 致謝 . . . . . . . . . . . . . . . . . . . . . . . i
中文摘要 . . . . . . . . . . . . . . . . . . . . . ii Abstract . . . . . . . . . . . . . . . . . . . . . iii List of Figures . . . . . . . . . . . . . . . . . . vii List of Tables . . . . . . . . . . . . . . . . . . viii Chapter 1 Introduction . . . . . . . . . . . . . . 1 1.1 Motivation . . . . . . . . . . . . . . . . . . 2 1.2 Contributions of the Thesis . . . . . . . . . . 2 1.3 Organizations of the Thesis . . . . . . . . . . 3 Chapter 2 Preliminaries . . . . . . . . . . . . . . 4 2.1 Propositional Satisfiability . . . . . . . . . 4 2.2 Finite State Transition System . . . . . . . . 4 2.3 Model Checking Problem . . . . . . . . . . . . 5 2.4 Bounded Model Checking . . . . . . . . . . . . 7 2.5 Property Directed Reachability . . . . . . . . 9 2.6 k-Inductive Invariant . . . . . . . . . . . . . 12 Chapter 3 PDR with Dynamic Timeframe Expansion . . 15 3.1 Motivation . . . . . . . . . . . . . . . . . . 15 3.2 Parallel Timeframe Expansion . . . . . . . . . 18 3.2.1 Overview . . . . . . . . . . . . . . . . . . 18 3.2.2 Intermediate State Constraints . . . . . . . 20 3.2.3 Implementation . . . . . . . . . . . . . . . 22 3.2.4 Soundness and Completeness . . . . . . . . . 25 3.3 Serial Timeframe Expansion . . . . . . . . . . 28 3.3.1 Overview . . . . . . . . . . . . . . . . . . 28 3.3.2 Intermediate State Constraints . . . . . . . 29 3.3.3 Implementation . . . . . . . . . . . . . . . 30 3.3.4 Soundness and Completeness . . . . . . . . . 32 3.4 Dynamic Timeframe Expansion . . . . . . . . . . 36 3.4.1 Overview . . . . . . . . . . . . . . . . . . 36 3.4.2 Decision Heuristic . . . . . . . . . . . . . 38 3.4.3 Implementation . . . . . . . . . . . . . . . 40 Chapter 4 Case Study . . . . . . . . . . . . . . . 42 4.1 Strength and Weakness . . . . . . . . . . . . . 42 4.2 A simple case . . . . . . . . . . . . . . . . . 43 4.2.1 Inductive Invariant by Parallel PDR . . . . . 45 4.2.2 Inductive Invariant by Serial PDR . . . . . . 46 4.3 A harder case . . . . . . . . . . . . . . . . . 46 Chapter 5 Experiment Results . . . . . . . . . . . 48 5.1 Parallel Timeframe Expansion . . . . . . . . . 48 5.2 Serial Timeframe Expansion . . . . . . . . . . 49 5.3 Dynamic Timeframe Expansion . . . . . . . . . . 51 5.4 Detailed Result . . . . . . . . . . . . . . . . 52 Chapter 6 Conclusion and Future Work . . . . . . . 57 References . . . . . . . . . . . . . . . . . . . . 59 | |
| dc.language.iso | en | |
| dc.subject | 模型檢查 | zh_TW |
| dc.subject | 正規驗證 | zh_TW |
| dc.subject | 可滿足性問題 | zh_TW |
| dc.subject | 時間框架延展 | zh_TW |
| dc.subject | 性質導向可達性技術 | zh_TW |
| dc.subject | Formal Verification | en |
| dc.subject | Model Checking | en |
| dc.subject | Satisfiability Problem | en |
| dc.subject | Property Directed Reachability | en |
| dc.subject | Timeframe Expansion | en |
| dc.title | 利用動態時間框架延展增進性質導向可達性技術 | zh_TW |
| dc.title | Improving Property Directed Reachability Using Dynamic Timeframe Expansion | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 105-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 江介宏(Jie-Hong Roland Jiang),許智仁(Jhih-Jen Hsu) | |
| dc.subject.keyword | 正規驗證,模型檢查,可滿足性問題,性質導向可達性技術,時間框架延展, | zh_TW |
| dc.subject.keyword | Formal Verification,Model Checking,Satisfiability Problem,Property Directed Reachability,Timeframe Expansion, | en |
| dc.relation.page | 60 | |
| dc.identifier.doi | 10.6342/NTU201702869 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2017-08-10 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
| 顯示於系所單位： | 電機工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-106-1.pdf 未授權公開取用 | 1.07 MB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。