臺灣博碩士論文加值系統

自從在2011年被提出後，性質導向可達性技術至今仍是最好的模型檢查演算法。但是仍有許多的案例是性質導向可達性技術難以解決的，因此，為了改進這個演算法，有許多的研究先後被發表。在這篇論文中，我們藉由獨立的檢查謂詞以輔助性質導向可達性演算法。此外，作為證明的例子，我們也提供了兩種能夠輕易從演算過程中得出的樣式。原本的性質導向可達性演算法與新方法皆被實作於Ia2b這個自製的模型檢查環境上。透過利用硬體模型檢查比賽的資料所做的實驗得知，我們所提出的方法能夠解出比原本的性質導向可達性技術更多的案例。

Since proposed in 2011, PDR (IC3) has been the best model checking algorithm until now. However, there are still many cases that PDR struggles to solve. Hence, many works are presented to enhance the algorithm. In this thesis, we propose a general method to aid PDR by solving predicate separately. Furthermore, we provide two kinds of useful pattern easily recognized from the solving process as example. The original PDR algorithm and the new feature are implemented on a custom model checking environment called Ia2b. The experiment on HWMCC benchmarks shows that our method can solve more cases than the classic PDR.

誌謝 i
中文摘要 ii
Abstract iii
Contents iv
List of Figures vi
List of Tables viii
1 Introduction 1
1.1 Contributions of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 Organizations of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . 3
2 Preliminaries 4
2.1 Propositional Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . 4
2.2 Finite State Boolean Transition System . . . . . . . . . . . . . . . . . . . 5
2.3 Model Checking Problem . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.4 Property Directed Reachability . . . . . . . . . . . . . . . . . . . . . . . 8
2.4.1 The Monotonicity of Frames . . . . . . . . . . . . . . . . . . . . 10
2.4.2 Ternary Simulation . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.4.3 Recursively Blocking Cubes . . . . . . . . . . . . . . . . . . . . 14
2.4.4 Propagating Blocked Cubes . . . . . . . . . . . . . . . . . . . . 15
2.4.5 Other Subroutines . . . . . . . . . . . . . . . . . . . . . . . . . 17
3 Predicate Extraction 18
3.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
3.2 General Method and Correctness . . . . . . . . . . . . . . . . . . . . . . 21
3.3 Two Kinds of Predicate . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.3.1 Blocking Clause . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.3.2 Proof Obligation . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.3.3 Recap for 6s288r . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4 Implementation 32
4.1 The Model Checking Environment . . . . . . . . . . . . . . . . . . . . . 32
4.2 Optimization and Other Things We Tried . . . . . . . . . . . . . . . . . 34
4.2.1 Subsumption . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4.2.2 Ternary Simulation . . . . . . . . . . . . . . . . . . . . . . . . . 35
4.2.3 SAT Query . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2.4 Storage of Proof Obligation . . . . . . . . . . . . . . . . . . . . 39
4.2.5 Propagating Cubes . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.2.6 Activity of State Variables . . . . . . . . . . . . . . . . . . . . . 41
4.2.7 Predicate Extraction . . . . . . . . . . . . . . . . . . . . . . . . 42
5 Experimental Results 45
5.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
5.2 Performance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
5.3 Detailed Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
6 Conclusion and Future Work 66
Reference 68

Randal E Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 100(8):677–691, 1986.
João P Marques-Silva and Karem A Sakallah. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506–521, 1999.
Hantao Zhang. Sato: An efficient propositional prover. In International Conference on Automated Deduction, pages 272–275. Springer, 1997.
Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Conference, pages 530–535, 2001.
E Goldberg and Y Novikov. Berkmin: A fast and robust sat-solver. In Proceedings 2002 Design, Automation and Test in Europe Conference and Exhibition, pages 142–149. IEEE, 2002.
Niklas Eén and Niklas Sörensson. An extensible sat-solver. In International conference on theory and applications of satisfiability testing, pages 502–518. Springer, 2003.
Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In Twenty-first International Joint Conference on Artificial Intelligence, 2009.
Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without bdds. In International conference on tools and algorithms for the construction and analysis of systems, pages 193–207. Springer, 1999.
Mary Sheeran, Satnam Singh, and Gunnar Stålmarck. Checking safety properties using induction and a sat-solver. In International conference on formal methods in computer-aided design, pages 127–144. Springer, 2000.
Niklas Eén and Niklas Sörensson. Temporal induction by incremental sat solving. Electronic Notes in Theoretical Computer Science, 89(4):543–560, 2003.
Kenneth L McMillan. Interpolation and sat-based model checking. In International Conference on Computer Aided Verification, pages 1–13. Springer, 2003.
William Craig. Linear reasoning. a new form of the herbrand-gentzen theorem. The Journal of Symbolic Logic, 22(3):250–268, 1957.
Yakir Vizel and Orna Grumberg. Interpolation-sequence based model checking. In 2009 Formal Methods in Computer-Aided Design, pages 1–8. IEEE, 2009.
Vijay D’Silva, Daniel Kroening, Mitra Purandare, and Georg Weissenbacher. Interpolant strength. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 129–145. Springer, 2010.
Simone Fulvio Rollini, Ondrej Sery, and Natasha Sharygina. Leveraging interpolant strength in model checking. In International Conference on Computer Aided Verification, pages 193–209. Springer, 2012.
Aaron R Bradley. Sat-based model checking without unrolling. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 70–87. Springer, 2011.
Aaron R Bradley and Zohar Manna. Checking safety by inductive generalization of counterexamples to induction. In Formal Methods in Computer Aided Design (FMCAD’07), pages 173–180. IEEE, 2007.
Niklas Een, Alan Mishchenko, and Robert Brayton. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD), pages 125–134. IEEE, 2011.
Hong-Syun Jiang and Chung-Yang (Ric) Huang. Enhancing property directed reachability technique through cube analysis. Master Thesis, National Taiwan University, 2015.
Kuan Fan, Ming-Jen Yang, and Chung-Yang Huang. Automatic abstraction refinement of tr for pdr. In 2016 21st Asia and South Pacific Design Automation Conference (ASP-DAC), pages 121–126. IEEE, 2016.
Ming-Jen Yang and Chung-Yang (Ric) Huang. Improving property directed reachability with temporal decomposition. Master Thesis, National Taiwan University, 2016.
Cheng-Han Yang and Chung-Yang (Ric) Huang. Improving property directed reachability using dynamic timeframe expansion. Master Thesis, National Taiwan University, 2017.
Shih-Yu Chuang and Chung-Yang (Ric) Huang. Property directed reachability with interpolation refinement. Master Thesis, National Taiwan University, 2019.
Alexander Ivrii and Arie Gurfinkel. Pushing to the top. In 2015 Formal Methods in Computer-Aided Design (FMCAD), pages 65–72. IEEE, 2015.
Ken L McMillan. Applying sat methods in unbounded symbolic model checking. In International Conference on Computer Aided Verification, pages 250–264. Springer, 2002.
Armin Biere. The aiger and-inverter graph (aig) format version 20071012. FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr, 69:4040, 2007.
Armin Biere, Keijo Heljanko, and Siert Wieringa. Aiger 1.9 and beyond. Available at fmv. jku. at/hwmcc11/beyond1. pdf, 2011.
Alan Mishchenko, Satrajit Chatterjee, Roland Jiang, and Robert K Brayton. Fraigs: A unifying representation for logic synthesis and verification. Technical report, ERL Technical Report, 2005.
Robert Brummayer and Armin Biere. Local two-level and-inverter graph minimization without blowup. Proc. MEMICS, 6:32–38, 2006.
Jordi Cortadella. Timing-driven logic bi-decomposition. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 22(6):675–685, 2003.
Niklas Eén and Armin Biere. Effective preprocessing in sat through variable and clause elimination. In International conference on theory and applications of satisfiability testing, pages 61–75. Springer, 2005.
Niklas Eén and Niklas Sörensson. The MiniSat Page. http://minisat.se/.
Gilles Audemard and Laurent Simon. Glucose’s home page. https://www.labri.fr/perso/lsimon/glucose/.
G. S. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic. Leningrad:Steklov Math. Institute, 1968.
David A Plaisted and Steven Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2(3):293–304, 1986.
Miroslav N Velev. Efficient translation of boolean formulas to cnf in formal verification of microprocessors. In ASP-DAC 2004: Asia and South Pacific Design Automation Conference 2004 (IEEE Cat. No. 04EX753), pages 310–315. IEEE, 2004.
Daniel Sheridan. The optimality of a fast cnf conversion and its use with sat. SAT, 2, 2004.
Niklas Een, Alan Mishchenko, and Niklas Sörensson. Applying logic synthesis for speeding up sat. In International Conference on Theory and Applications of Satisfiability Testing, pages 272–286. Springer, 2007.
Alberto Griggio and Marco Roveri. Comparing different variants of the ic3 algorithm for hardware model checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 35(6):1026–1039, 2015.
Robert Brayton and Alan Mishchenko. Abc: An academic industrial-strength verification tool. In International Conference on Computer Aided Verification, pages 24–40. Springer, 2010.
Cheng-Yin Wu and Chung-Yang (Ric) Huang. V3: An extensible framework for hardware verification. https://github.com/chengyinwe/V3.
Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. https://people.eecs.berkeley.edu/~alanmi/abc/.