臺灣博碩士論文加值系統

性質導向可達性技術自從在2011年被發表之後，一直是最有效率的模型驗證演算法。不像其他的演算法往往只偏向於安全或不安全的案例其中一者，性質導向可達性技術對於兩者都能有不錯的效能。然而，仍然有些案例是難以被解決的，所以一直有對於如何改進性質導向可達性技術的研究。在這篇論文中，我們提出了兩種將有界模型驗證融合進性質導向可達性技術的方法，以及一種結合原本的性質導向可達性技術和以上兩種演算法的混合演算法。我們在V3的框架上實做了我們的演算法，並用硬體模型驗證競賽的案例進行測試。實驗結果指出我們的演算法可以在較短的時間內解出比原本的演算法還多的案例。

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.

致謝 . . . . . . . . . . . . . . . . . . . . . . . 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

[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.