Abstract
This paper addresses the problem of reducing the size of Craig interpolants generated within inner steps of SAT-based Unbounded Model Checking. Craig interpolants are obtained from refutation proofs of unsatisfiable SAT runs, in terms of and/or circuits of linear size, w.r.t. the proof. Existing techniques address proof reduction, whereas interpolant circuit compaction is typically considered as an implementation problem, tackled with standard logic synthesis techniques. We propose a three step interpolant computation process, specifically oriented to scalability, in which we: (1) exploit an existing technique to detect and remove redundancies in refutation proofs, (2) apply customized light weight combinational logic reductions (constant propagation, ODC-based simplifications, and BDD-based sweeping) directly on the proof graph data structure, (3) introduce an ad-hoc combinational reduction procedure for large interpolant circuits, based on the incrementality and divide-and-conquer paradigms. The main contributions of our approach are represented by the overall approach, the proposed combinational reduction technique, and a detailed experimental evaluation of the interpolant generation process, on a set of benchmarks from the Hardware Model Checking Competitions 2013 and 2014.
Similar content being viewed by others
Notes
we use the transposed graph \({\varPi }^T\) here, as reverse edges are needed, formally, to identify sub-trees
Another motivation for our choice is the fact that AIGER is the netlist interchange format chosen for Hardware Model Checking Competitions [5]
Forward and backward directions refer to the interpolant circuit. Forward thus follows edges in \(\varPi \), whereas backward follows edges in \(\varPi ^T\).
Balancing is a linear-time DAG-rewriting, based on identifying unbalanced sub-trees of AND (resp OR) gates.
The overall purpose of POpt6 is to enforce local ODC reductions, by trying different orderings within AND (resp. OR) groups of nodes. So it is basically a variant of POpt5 with higher overhead, and more compaction expected.
PdTrav, though disqualified for an unsound result, globally ranked second.
References
Craig W (1957) Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J Symb Log 22(3):269–285
Pacific Journal of Mathematics RC (1959) An interpolation theorem in the predicate calculus. Pac J Math 9:155–164
McMillan KL (2003) Interpolation and SAT-based model checking. In: Proceedings of the computer aided verification, vol 2725 of LNCS. Springer, Boulder, CO, USA, pp 1–13
Bradley AR (2011) Sat-based model checking without unrolling. VMCAI. Springer, Austin, TX, pp 70–87
Biere A, Jussila T. The model checking competition web page, http://fmv.jku.at/hwmcc
McMillan KL, Jhala R (2005) Interpolation and SAT-based model checking. In: T. Ball, R.B. Jones (eds) Proceeding of the computer aided verification, vol 3725 of LNCS. Springer, Edinburgh, pp 39–51
Marques-Silva J (2005) Improvements to the implementation of Interpolant-Based Model Checking. In: D. Borrione, W. Paul (eds) Proceedings of the correct hardware design and verification methods, vol 3725 of LNCS. Springer, Edinburgh, pp 367–370
Cabodi G, Murciano M, Nocco S, Quer S (2008) Boosting interpolation with dynamic localized abstraction and redundancy removal. ACM Trans Des Autom Electron Syst 13(1):309–340
Cabodi G, Camurati P, Murciano M (2008) Automated abstraction by incremental refinement in interpolant-based model checking. In: Proceedings of the internaional conference on computer-aided design. ACM Press, San Jose, CA, pp 129–136
Li B, Somenzi F (2006) Efficient abstraction refinement in interpolation-based unbounded model checking. In: Tools and algorithms for the construction and analysis of systems. vol 3920, pp 227–241
D’Silva V, Purandare M, Kroening D (2008) Approximation refinement for interpolation-based model checking. In: F. Logozzo, D. Peled, L.D. Zuck (eds) Verification, model checking and abstract interpretation. Lecture notes in computer science, vol 4905, Springer, pp 68–82
Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7:201–215
Davis M, Logemann G, Loveland D (1962) A machine procedure for theorem-proving. J ACM 5:394–397
Marques-Silva JP, Sakalla KA (1996) GRASP— A new search algorithm for satisfiability. In: Proceedings of the international conference on tool with artificial intelligence
Zhang L, Malik S (2003) Validating sat solvers using an independent resolution-based checker: practical implementations and other applications. In: Proceedings of the conference on design, automation and test in Europe, vol 1. DATE ’03, IEEE Computer Society 10880, Washington, DC
Bar-Ilan O, Fuhrmann O, Hoory S, Shacham O, Strichman O (2009) Linear-time reductions of resolution proofs, vol 5394. Springer, Berlin, pp 114–128
Rollini SF, Bruttomesso R, Sharygina N (2010) An efficient and flexible approach to resolution proof reduction. In: Haifa verification conference (HVC), Springer, Haifa
Fontaine P, Merz S, Paleo BW (2011) Compression of propositional resolution proofs via partial regularization. In: Proceedings of the automated deduction - CADE-23 - 23rd international conference on automated deduction, Wroclaw, Poland, July 31– August 5, 2011, pp 237–251
Gupta A. (2012) Improved single pass algorithms for resolution proof reduction. In: ATVA, pp 107–121
Cotton S. (2010) Two techniques for minimizing resolution proofs. In: Proceedings of the theory and applications of satisfiability testing - SAT 2010, 13th international conference, SAT 2010, Edinburgh, UK, July 11–14, 2010, pp 306–312
Saluja N, Khatri SP (2004) A robust algorithm for approximate compatible observability don’t care computation. In: Proceedings design automation conference, pp 422–427
Savoj H, Brayton RK (1990) The use of observability and external don’t cares for the simplification of multi-level networks. In: Proceedings of the design automation conference, pp 297–301
Savoj H, Brayton RK, Touati HJ (1991) Extracting local don’t cares for network optimization. In: ICCAD, pp 514–517
Mishchenko A, Brayton RK (2007) Sat-based complete don’t-care computation for network optimization. CoRR Arxiv:0710.4695
McMillan KL (2002) Applying sat methods in unbounded symbolic model checking. In: E Brinksma, KG Larsen (eds) CAV, Lecture notes in computer science, vol 2404. Springer, pp 250–264
McMillan KL, Labs CB (2005) Don’t-care computation using k-clause approximation. In: International Workshop on Logic & Synthesis
Brayton RK, Mishchenko A (2010) Abc: An academic industrial-strength verification tool. In: T Touili, B Cook, P Jackson (eds) CAV, Lecture notes in computer science, vol 6174, Springer, pp 24–40
Mishchenk A (2005) ABC: A system for sequential synthesis and verification, http://www.eecs.berkeley.edu/~alanmi/abc/
Cabodi G, Loiacono C, Vendraminetto D (2013) Optimization techniques for craig interpolant compaction in unbounded model checking. In: Proceedings of the design automation & test in Europe conference, IEEE Computer Society, Grenoble, France, pp 1417–1422
Bruttomesso R, Rollini SF, Sharygina N, Tsitovich A (2010) Flexible interpolation with local proof transformations. In: International conference of computer aided design (ICCAD), IEEE Computer Society, San Jose, USA
Sharygina N (2013) PeRIPLO. Formal verification at University of Lugano, http://verify.inf.unisi.ch/periplo.html
Bloem R, Malik S, Schlaipfer M, Weissenbacher G (2014) Reduction of resolution refutations and interpolants via subsumption. In: Proceedings of the hardware and software: verification and testing - 10th international Haifa verification conference, HVC 2014, Haifa, Israel, November 18–20, 2014, pp 188–203
Chockler H, Ivril A, Matsliah A (2012) Computing interpolants without proofs. In: Proceedings of the 7th international Haifa verification conference on hardware and software: verification and testing. HVC ’12
Vizel Y, Ryvchin V, Nadel A (2013) Efficient generation of small interpolants in cnf. In: CAV, pp 330–346
Vizel Y, Gurfinkel A (2014) Interpolating property directed reachability. CAV, pp 260–276
Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th design automation conference, IEEE Computer Society, Las Vegas, NV
Eén N, Sörensson N (2009) The minisat SAT solver, http://minisat.se
Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th design automation conference, IEEE Computer Society, New Orleans, LA, pp 317–320
Eén N (May 2007) Cut sweeping. Technical report, Cadence Research Labs, Berkeley, USA
Kuehlmann A, Krohm F (1997) Equivalence checking using cuts and heaps. In: Proceedings of the 34th design automation conference, IEEE Computer Society, Anaheim, CA, pp 263–268
Kuehlmann A (2004) Dynamic transition relation simplification for bounded property checking. In: Proceedings of the international conference on computer-aided design, IEEE Computer Society, San Jose, CA, pp 50–57
Bjesse P, Boralv A (2004) DAG-aware circuit compression for formal verification. In: Proceedings of the international conference on computer-aided design, IEEE Computer Society, San Jose, CA
Brayton RK, Chatterjee S, Mishchenko A (2006) DAG-aware aig rewriting: a fresh look at combinational logic synthesis. In: Proceedings design automation conference, pp 532–536
Mishchenko A, Chatterjee S, Brayton R (2006) Dag-aware aig rewriting: a fresh look at combinational logic synthesis. In: In DAC 06— Proceedings of the 43rd annual conference on design automation, ACM Press, pp 532–536
Cabodi G, Nocco S, Quer S (2011) Benchmarking a model checker for algorithmic improvements and tuning for performance. Form Methods Syst Des 39(2):205–227
Formal-Methods-Group (2014) PdTrav Tool, http://fmgroup.polito.it/index.php/download/viewcategory/3-pdtrav-package
Biere A, Heljanko K (2014) The model checking competition web page, http://fmv.jku.at/hwmcc14
Acknowledgments
This work was supported in part by SRC contract 2009-TJ-1968
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Cabodi, G., Loiacono, C. & Vendraminetto, D. Optimization techniques for craig interpolant compaction in unbounded model checking. Form Methods Syst Des 46, 135–162 (2015). https://doi.org/10.1007/s10703-015-0229-0
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-015-0229-0