To further understand the effect of our method, we perform a series of analysis in order to find the relationship between the characteristic of predicate solving and the improvement.
There are two kinds of comparison. The first one is to compare the basic PDR with the one activating one of the two predicates. The second one is to compare between the two predicates. We first introduce the information extracted from the process.
1. Total_Pre: The number of predicates that is ever tried to prove.
2. PASS: The number of predicates successfully proved to be unreachable (safe).
3. Total_Pre_Inf: Total number of clauses in the inductive set produced by all the separate PDRs to solve predicate.
4. Added: Total number of clauses added back to the original PDR. After terminating the separate PDR, only the clause that is not subsumed by F∞can be added back to the original one.
5. Total_Inf: Total number of clauses added to F∞of the original PDR throughout the process. This number includes the clauses counted in Added.
6. Cls_Length: Average number of literals for the clauses counted in Total_Inf.
7. Cls_Length_Pre: Average number of literals for the clauses counted in Added.
8. Runtime: Runtime for this configuration of PDR.
9. SAT_Query_Pre: The number of SAT query called by all the separate PDRs.
Note that the above numbers are extracted from the PDR with predicate solving since we want to find a better criterion to choose predicate. We only pick the runtime of basic PDR to show the improvement. Then we introduce the combination of the above numbers that we think meaningful.
1. Improvement: The comparison between the Runtime of basic PDR (oldTime) and that of the PDR with predicate solving (newTime). The improvement is equal to (oldTime - newTime) / Max(oldTime, newTime). PDR with predicate solving is more efficient iff the value is positive. In addition, if either one is timeout, the absolute value will be one. Last, in order to prevent noise, we do not consider the case that both of the configurations take less than five seconds. On the other hand, we only consider that one is faster than the other when comparing clause-based and obligation-based predicate.
2. Added / Total_Inf: The proportion of clauses in F∞added from the separate PDR.
It is to show that how important the separate PDR plays the role for the original one.
3. Added / (Total_Inf * SAT_Query_Pre): The proportion of clauses in F∞added from the separate PDR per SAT query. It is to show that how important one SAT query for separate PDR can contribute to the original one.
4. PASS / Total_Pre: The proportion of successful predicate.
5. Added / Total_Pre_Inf: The proportion of clauses produced by the separate PDR that can be added back. It is to show the ability that the separate PDR can explore different kinds of clause.
6. Added / SAT_query_Pre: The number of clauses added back to the original PDR per SAT query. It is to show that how efficient the separate PDR can generate useful clause.
7. Cls_Length_Pre / Cls_Length: The ratio of average length of clauses produced by the original and separate PDR. For a single clause, we think it excludes more states if it has shorter length and we call it stronger. It is to show which kinds of clause is stronger.
For the comparison of basic PDR and the one with predicate solving, there is no obvious target to predict the improvement. The even distribution takes place for both of
the predicates. Although we have difficulty identifying good predicate to maximize the benefits, we can still find some property about it. On the other hand, when comparing the two kinds of predicate, we can roughly distinguish the characteristic of efficiency for some cases, which provides us a way to choose between the predicates. In the following, we display some of the figures to demonstrate the analysis. In all the figures, each spot corresponds to a case. Furthermore, the experiment in this section only contains pdr_vb.
Figure 5.13: The comparison between clause-based and obligation-based predicate. X-axis is for clause and Y-X-axis is for obligation. The data are Added / Total_Inf and Added / (Total_Inf * SAT_Query_Pre) and both of them are in log scale since the range of value is too wide to use linear scale. The figure is designed to be square to highlight the comparison. Green spot means clause-based predicate is more efficient and red one for obligation. There is no obvious boundary in the left subfigure. However, for the right subfigure, we can roughly find that the predicate is more efficient if the value is larger.
That is, if we divide the square into two triangles by the line y = x, green spots mainly concentrate at the lower-right triangle, and vice versa.
Figure 5.14: The comparison between basic PDR and clause-based predicate (1). Y-axis is the improvement and X-axis denotes the data including Added / Total_Inf and Added / (Total_Inf * SAT_Query_Pre). Both of the data are in log scale. There is no obvious target since almost for every value in X-axis, there exist positive and negative values for Y-axis.
In other words, we cannot distinguish which range of value can lead to improvement.
Figure 5.15: The comparison between basic PDR and clause-based predicate (2). Y-axis is the improvement and X-axis is PASS / Total_Pre. There is no obvious target. Note that the proportion of PASS is actually very low, so the improvement can also result from the predicate that fails or aborts.
Figure 5.16: The comparison between basic PDR and obligation-based predicate. Y-axis is the improvement and X-axis is Cls_Length_Pre / Cls_Length. There is no obvious target. Note that the average length of clauses for separate PDR is often shorter than that
Chapter 6
Conclusion and Future Work
In this thesis, we propose a flexible method to solve predicate separately. In addition, we provide two examples of useful predicate identified from blocking clauses and proof obligations. We show by the experiment that this method is efficient compared to the original PDR. Although we achieve a good result at the first step, there are still many works to do.
We have shown that there exists a trend for predicate solving. An important job is to find the absolutely best value for all the parameters. However, the values may be case-dependent and vary among different sets of benchmarks. We then modify the goal to find a fast and effective way to identify the best combination under a given set of circuits. On the other hand, since the case-dependency, another choice is to find a good heuristic to change the value dynamically. This again rely on the local information to do the modification.
On top of the two kinds of relatively general predicate we present, there may exists many other possibilities due to the variety of the circuit characteristics. By creating more and more patterns as predicate, we expect to answer more unsolved cases by the support of different one. Then the rest problem is to combine them automatically. As the experiment, simply activating all the predicates is not a guarantee of improvement. We provide two possible solutions here. The first one is to use multi-threads in parallel.
Every thread is associated with its own kind of predicate and is not interrupted by the other ones. The second one is more aggressive to integrate to a single engine. We use local information again to trigger the corresponding predicate. Hence, the activated predicate may be different throughout the process. There is also possible to be no or more than one predicate at a time.
As indicated in Subsection 4.2.7, we can merge all the clauses back after solving the predicate. That is, we are not limited by F∞. A possible scheme is when observing similar clauses in a frame. We can change the termination criteria to be up to that frame.
If reaching that frame successfully, we know the common part is unreachable up to that frame. Hence, we get a trace of frame that can eliminate all the similar clauses at that frame, which leads to a smoother representation of the reachability.
Reference
[1] Randal E Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 100(8):677–691, 1986.
[2] 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.
[3] Hantao Zhang. Sato: An efficient propositional prover. In International Conference on Automated Deduction, pages 272–275. Springer, 1997.
[4] 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.
[5] 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.
[6] 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.
[7] Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In Twenty-first International Joint Conference on Artificial Intelligence, 2009.
[8] 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.
[9] 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.
[10] Niklas Eén and Niklas Sörensson. Temporal induction by incremental sat solving.
Electronic Notes in Theoretical Computer Science, 89(4):543–560, 2003.
[11] Kenneth L McMillan. Interpolation and sat-based model checking. In International Conference on Computer Aided Verification, pages 1–13. Springer, 2003.
[12] William Craig. Linear reasoning. a new form of the herbrand-gentzen theorem. The Journal of Symbolic Logic, 22(3):250–268, 1957.
[13] Yakir Vizel and Orna Grumberg. Interpolation-sequence based model checking. In 2009 Formal Methods in Computer-Aided Design, pages 1–8. IEEE, 2009.
[14] 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.
[15] 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.
[16] Aaron R Bradley. Sat-based model checking without unrolling. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 70–
87. Springer, 2011.
[17] 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.
[18] 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.
[19] Hong-Syun Jiang and Chung-Yang (Ric) Huang. Enhancing property directed reachability technique through cube analysis. Master Thesis, National Taiwan University, 2015.
[20] 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.
[21] Ming-Jen Yang and Chung-Yang (Ric) Huang. Improving property directed reachability with temporal decomposition. Master Thesis, National Taiwan University, 2016.
[22] Cheng-Han Yang and Chung-Yang (Ric) Huang. Improving property directed reachability using dynamic timeframe expansion. Master Thesis, National Taiwan University, 2017.
[23] Shih-Yu Chuang and Chung-Yang (Ric) Huang. Property directed reachability with interpolation refinement. Master Thesis, National Taiwan University, 2019.
[24] Alexander Ivrii and Arie Gurfinkel. Pushing to the top. In 2015 Formal Methods in Computer-Aided Design (FMCAD), pages 65–72. IEEE, 2015.
[25] Ken L McMillan. Applying sat methods in unbounded symbolic model checking. In International Conference on Computer Aided Verification, pages 250–264. Springer, 2002.
[26] 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.
[27] Armin Biere, Keijo Heljanko, and Siert Wieringa. Aiger 1.9 and beyond. Available at fmv. jku. at/hwmcc11/beyond1. pdf, 2011.
[28] 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.
[29] Robert Brummayer and Armin Biere. Local two-level and-inverter graph minimization without blowup. Proc. MEMICS, 6:32–38, 2006.
[30] Jordi Cortadella. Timing-driven logic bi-decomposition. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 22(6):675–685, 2003.
[31] 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.
[32] Niklas Eén and Niklas Sörensson. The MiniSat Page. http://minisat.se/.
[33] Gilles Audemard and Laurent Simon. Glucose’s home page. https://www.labri.fr/
perso/lsimon/glucose/.
[34] G. S. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic. Leningrad:Steklov Math.
Institute, 1968.
[35] David A Plaisted and Steven Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2(3):293–304, 1986.
[36] Miroslav N Velev. Efficient translation of boolean formulas to cnf in formal
Automation Conference 2004 (IEEE Cat. No. 04EX753), pages 310–315. IEEE, 2004.
[37] Daniel Sheridan. The optimality of a fast cnf conversion and its use with sat. SAT, 2, 2004.
[38] 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.
[39] 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.
[40] Robert Brayton and Alan Mishchenko. Abc: An academic industrial-strength verification tool. In International Conference on Computer Aided Verification, pages 24–40. Springer, 2010.
[41] Cheng-Yin Wu and Chung-Yang (Ric) Huang. V3: An extensible framework for hardware verification. https://github.com/chengyinwe/V3.
[42] Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. https://people.eecs.berkeley.edu/~alanmi/abc/.