臺灣博碩士論文加值系統

因為對於安全或是不安全的案例都有突出的效能，性質導向可達性技術從二零一一年發表以來一直是模式驗證問題中最有效率的演算法。然而，因為模式驗證問題本質上的高複雜度，還是有許多的案例沒有被驗證。因此，改善性質導向可達性技術的研究是一個非常重要的主題，近來也產生了許多相關的研究。在這篇論文中，我們提出了三種基於將時態分解技術的概念融合於性質導向可達性技術的創新方法。我們將我們所提出的方法實作於“驗證三”的驗證架構中，並且使用世界”硬體模式驗證競賽”的案例與原本的性質導向可達性技術做比較。實驗結果顯示我們的方法可以驗證許多原本未被驗證的案例，對不安全的案例有一點四倍的運作時間提升，代表著這些方法可以與原本的性質導向可達性技術在相當多的基準點上互補。

Property Directed Reachability has always been the most efficient algorithm for the safety property checking problem for its well performance on both safe and unsafe case since its publication in 2011. However, there are still a large number of cases remaining unsolved due to the intrinsic high complexity of model checking problem. Therefore, improving PDR is an important subject and attracts lots of research recently. In this paper, we present three novel approaches that integrate a sequential optimization technique, called temporal decomposition into PDR. We implemented our work in V3 and compared to original PDR in V3 on HWMCC benchmarks. The experimental result shows that the proposed methods solved many originally unsolved cases, and improved unsafe cases by 1.4x in runtimes. It means that these methods can complement original PDR on a large set of benchmarks.

誌謝 i
中文摘要 iv
ABSTRACT v
CONTENTS vi
LIST OF FIGURES viii
LIST OF TABLES ix
Chapter 1 Introduction 1
1.1 Motivation 2
1.2 Contributions of the Thesis 3
1.3 Organization of the Thesis 3
Chapter 2 Preliminaries 5
2.1 Propositional Satisfiability 5
2.2 Finite State Transition System 6
2.3 Model Checking Problem 6
2.4 Property Directed Reachability 7
2.5 Temporal Decomposition 10
2.5.1 Transient signals 11
2.5.2 Initialization inputs 14
Chapter 3 PDR with Temporal Decomposition 15
3.1 Motivation 15
3.2 Forward Reachability Constraint 17
3.3 Time-shifted PDR 18
3.3.1 Combine with transient signals 24
3.3.2 Deep-Shift 24
3.4 Multi-Step PDR 24
3.4.1 Activation condition 26
3.5 Soundness and Completeness 26
Chapter 4 Experimental Results 29
4.1 Time-Shifted PDR 29
4.1.1 Combine with transient signals 32
4.1.2 Forward Reachability Constraint 36
4.2 Multi-Step PDR 37
Chapter 5 Conclusion and Future Work 39
REFERENCE 41

[1]Clarke, Edmund M., Orna Grumberg, and Doron Peled. Model checking. MIT press, 1999.
[2]McMillan, Kenneth L. "Symbolic model checking." Symbolic Model Checking. Springer US, 1993. 25-60.
[3]Sheeran, Mary, Satnam Singh, and Gunnar Stålmarck. "Checking safety properties using induction and a SAT-solver." International conference on formal methods in computer-aided design. Springer Berlin Heidelberg, 2000.
[4]McMillan, Kenneth L. "Interpolation and SAT-based model checking. "International Conference on Computer Aided Verification. Springer Berlin Heidelberg, 2003.
[5]Bradley, Aaron R. "SAT-based model checking without unrolling." International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer Berlin Heidelberg, 2011.
[6]Een, Niklas, Alan Mishchenko, and Robert Brayton. "Efficient implementation of property directed reachability." Formal Methods in Computer-Aided Design (FMCAD), 2011. IEEE, 2011.
[7]Brayton, Robert, and Alan Mishchenko. "ABC: An academic industrial-strength verification tool." International Conference on Computer Aided Verification. Springer Berlin Heidelberg, 2010.
[8]Cheng-Yin Wu and Chung-Yang (Ric) Huang. “V3: An extensible framework for hardware verification”, https://github.com/chengyinwu/V3.
[9]Hardware model checking competition. http://fmv.jku.at/hwmcc/.
[10]Fan, Kuan, Ming-Jen Yang, and Chung-Yang Huang. "Automatic abstraction refinement of TR for PDR." 2016 21st Asia and South Pacific Design Automation Conference (ASP-DAC). IEEE, 2016.
[11]Ivrii, Alexander, and Arie Gurfinkel. "Pushing to the top." Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design. FMCAD Inc, 2015.
[12]Hong-Syun Jiang and Chung-Yang (Ric) Huang. “Enhancing Property Directed Reachability Technique through Cube Analysis.” Master Thesis. National Taiwan University, 2015.
[13]Vizel, Yakir, and Arie Gurfinkel. "Interpolating property directed reachability."International Conference on Computer Aided Verification. Springer International Publishing, 2014.
[14]Backes, John D., and Marc D. Riedel. "Using cubes of non-state variables with property directed reachability." Proceedings of the Conference on Design, Automation and Test in Europe. EDA Consortium, 2013.
[15]Case, Michael L., et al. "Enhanced verification by temporal decomposition."Formal Methods in Computer-Aided Design, 2009. FMCAD 2009. IEEE, 2009.