More Web Proxy on the site http://driver.im/

research-article

Boosting interpolation with dynamic localized abstraction and redundancy removal

Authors:

Gianpiero Cabodi,

Marco Murciano,

Stefano QuerAuthors Info & Claims

ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 13, Issue 1

Article No.: 3, Pages 1 - 20

https://doi.org/10.1145/1297666.1297669

Published: 06 February 2008 Publication History

Abstract

SAT--based Unbounded Model Checking based on Craig Interpolants is often able to overcome BDDs and other SAT--based techniques on large verification instances. Based on refutation proofs generated by SAT solvers, interpolants provide compact circuit representations of state sets, as they abstract away several nonrelevant details of the proofs. We propose three main contributions, aimed at controlling interpolant size and traversal depth. First of all, we introduce interpolant--based dynamic abstraction to reduce the support of computed interpolants. Subsequently, we propose new advances in interpolant compaction by redundancy removal. Finally, we introduce interpolant computation exploiting circuit quantification, instead of SAT refutation proofs. These techniques heavily rely on an effective application of the incremental SAT paradigm. The experimental results proposed in this paper are specifically oriented to prove properties, rather than disproving them, i.e., they target complete verification instead of simply hunting bugs. They show how this methodology is able to stretch the applicability of interpolant--based Model Checking to larger and deeper verification instances.

References

[1]

Abdulla, P. A., Bjesse, P., and Een, N. 2000. Symbolic reachability analysis based on SAT-solvers. In Tools and Algorithms for the Construction and Analysis of Systems, M. I. S. Susanne Graf, Ed. Vol. 1785. Springer-Verlag, Berlin, Germany, 411--425.

Digital Library

[2]

Berkelaar, M. and van Eijk, K. 2002. Efficient and effective redundancy removal for million-gate circuits. In Proceedings of the Design Automation & Test in Europe Conference. Paris, France, IEEE Computer Society, 1088--1088.

Digital Library

[3]

Biere, A., Cimatti, A., Clarke, E. M., Fujita, M., and Zhu, Y. 1999. Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of the 36th Design Automation Conference. New Orleans, LO, IEEE Computer Society, 317--320.

Digital Library

[4]

Bjesse, P., Leonard, T., and Mokkedem, A. 2001. Finding bugs in an alpha microprocessor using satisfiability solvers. In Proceedings of the International Conference on Computer Aided Verification. Paris, France, G. Berry, H. Comon, and A. Finkel, Eds. Lecture Notes in Computer Science, vol. 2102. Springer-Verlag, 454--464.

Digital Library

[5]

Bryant, R. E. 1986. Graph--based algorithms for Boolean function manipulation. IEEE Trans. Comput. C--35, 8, 677--691.

Digital Library

[6]

Burch, J. R., Clarke, E. M., Long, D. E., McMillan, K. L., and Dill, D. L. 1994. Symbolic model checking for sequential circuit verification. IEEE Trans. Comput.-Aid. Des. 13, 4, 401--424.

Digital Library

[7]

Cabodi, G., Nocco, S., and Quer, S. 2005. Circuit based quantification: back to state set manipulation within unbounded model checking. In Proceedings of the Design Automation and Test in Europe Conference. Munich, Germany, IEEE Computer Society.

Digital Library

[8]

Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., and Wang, D. 2002. Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In Proceedings of the Formal Methods in Computer-Aided Design. Portland, OR, M. D. Aagaard and J. W. O'Leary, Eds. Lecture Notes in Computer Science, vol. 2517. Springer, 35--51.

Digital Library

[9]

Cho, H., Hachtel, G., Jeong, S. W., Plessier, B., Schwarz, E., and Somenzi, F. 1990. ATPG aspects of FSM verification. In Proceedings of the International Conference on Computer-Aided Design. San Jose, CA, 134--137.

[10]

Coudert, O., Berthet, C., and Madre, J. C. 1989. Verification of sequential machines using Boolean function vectors. In Proceedings of the International Federation for Information Processing Workshop on Applied Formal Methods for Correct VLSI Design. Vol. 1. 111--128.

[11]

Coudert, O. and Madre, J. C. 1991. Symbolic computation of the valid states of the sequential machine: Algorithms and discussion. In International Workshop on Formal Methods in VLSI Design.

[12]

Eén, N. and Sörensson, N. 2003a. Minisat SAT Solver. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/.

[13]

Eén, N. and Sörensson, N. 2003b. Temporal induction by incremental sat solving. In Proceedings of the 1st International Workshop on Bounded Model Checking (BMC). Boulder, CO.

[14]

Ganai, M. K., Gupta, A., and Ashar, P. 2004. Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In Proceedings of the International Conference on Computer-Aided Design. San Jose, CA. IEEE Computer Society.

Digital Library

[15]

IBM. 2003. Ibm formal verification benchmark library. http://www.haifa.il.ibm.com/projects/verification/rb_homepage/benchmarks.html.

[16]

Kang, H. J. and Park, L. C. 2003. SAT-based unbounded symbolic model checking. In Proceedings of the 40th Design Automation Conference. Anaheim, CA. IEEE Computer Society, 840--843.

Digital Library

[17]

Kurshan, R. P. 1994. Computer aided verification of coordinating processes. Princeton University Press, Princeton, NJ.

Digital Library

[18]

Lin, B., Wang, C., and Somenzi, F. 2003. A satisfiability-based approach to abstraction refinement in model checking. In 1st International Workshop on Bounded Model Checking (BMC). Boulder, CO.

[19]

Manquinho, V. and Marques-Silva, J. 2002. Search pruning techniques in SAT--based branch-and-bound algorithms for the Binate covering problem. IEEE Trans. Comput.-Aid. Des. 21, 505--516.

Digital Library

[20]

Marques-Silva, J. 2005. Improvements to the implementation of interpolant--based model checking. In Proceedings of the Computer Aided Verification. Edinburgh, Scotland, UK. D. Borrione and W. Paul, Eds. Lecture Notes in Computer Science, vol. 3725. Springer, 367--370.

Digital Library

[21]

McMillan, K. L. 2002. Applying SAT methods in unbounded symbolic model checking. In Proceedings of the Computer Aided Verification. Copenhagen, Denmark, E. Brinksma and K. G. Larsen, Eds. Lecture Notes in Computer Science, vol. 2404. Springer, 250--264.

Digital Library

[22]

McMillan, K. L. 2003. Interpolation and SAT-based model checking. In Proceedings of the Computer Aided Verification. Boulder, CO, W. A. H. Jr. and F. Somenzi, Eds. Lecture Notes in Computer Science, vol. 2725. Springer, 1--13.

[23]

McMillan, K. L. and Jhala, R. 2005. Interpolation and SAT-based model checking. In Proceedings of the Computer Aided Verification. Edinburgh, Scotland, UK. T. Ball and R. B. Jones, Eds. Lecture Notes in Computer Science, vol. 3725. Springer, 39--51.

[24]

Mishchenko, A. 2005. ABC: A system for sequential synthesis and verification, http://www.eecs.berkeley.edu/~alanmi/abc/.

[25]

Mishchenko, A. and Brayton, R. K. 2006a. Improvements to combinational equivalence checking. In Proceedings of the International Conference on Computer-Aided Design. San Jose, CA. ACM Press.

Digital Library

[26]

Mishchenko, A. and Brayton, R. K. 2006b. Scalable logic synthesis using a simple circuit structure. In Proceedings of the International Workshop on Logic Synthesis. Lake Tahoe, CA.

[27]

Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., and Malik, S. 2001. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference. Las Vegas, NV. IEEE Computer Society.

Digital Library

[28]

Sheeran, M., Singh, S., and Stålmarck, G. 2000. Checking safety properties using induction and SAT solver. In Proceedings of the Formal Methods in Computer-Aided Design. Austin, TX, W. A. Hunt and S. D. Johnson, Eds. Lecture Notes in Computer Science, vol. 1954. Springer-Verlag, 108--125.

Digital Library

[29]

Whittemore, J., Kim, J., and Sakallah, K. 2001. Satire: A new incremental satisfiability engine. In Proceedings of the 38th Design Automation Conference. ACM Press, 542--545.

Digital Library

[30]

Williams, P. F., Biere, A., Clarke, E. M., and Gupta, A. 2000. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In Proceedings of the Computer Aided Verification. Chicago, IL, E. A. Emerson and A. P. Sistla, Eds. Lecture Notes in Computer Science, vol. 2102. Springer-Verlag. 124--138.

Digital Library

Cited By

Cabodi GCamurati PPalena MPasini P(2022)Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checkingFormal Methods in System Design10.1007/s10703-022-00406-760:2(117-146)Online publication date: 8-Dec-2022
https://dl.acm.org/doi/10.1007/s10703-022-00406-7
Cabodi GCamurati PPalena MPasini PVendraminetto D(2020)Reducing Interpolant Circuit Size Through SAT-Based WeakeningIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2019.291531739:7(1524-1531)Online publication date: 17-Jun-2020
https://dl.acm.org/doi/10.1109/TCAD.2019.2915317
Cabodi GCamurati PPalena MPasini PVendraminetto D(2019)Logic Synthesis for Interpolant Circuit CompactionIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2018.280822938:2(380-384)Online publication date: Feb-2019
https://doi.org/10.1109/TCAD.2018.2808229
Show More Cited By

Index Terms

Boosting interpolation with dynamic localized abstraction and redundancy removal
1. Hardware
  1. Integrated circuits
    1. Logic circuits

Recommendations

SAT-based counterexample-guided abstraction refinement

We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" ...
Abstraction for model checking multi-agent systems

Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel ...
PVS Strategies for Proving Abstraction Properties of Automata

Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct abstraction relation between the states of the automata, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Design Automation of Electronic Systems

ACM Transactions on Design Automation of Electronic Systems Volume 13, Issue 1

January 2008

496 pages

ISSN:1084-4309

EISSN:1557-7309

DOI:10.1145/1297666

Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 06 February 2008

Accepted: 01 July 2007

Revised: 01 June 2007

Received: 01 June 2006

Published in TODAES Volume 13, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
286
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)1

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cabodi GCamurati PPalena MPasini P(2022)Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checkingFormal Methods in System Design10.1007/s10703-022-00406-760:2(117-146)Online publication date: 8-Dec-2022
https://dl.acm.org/doi/10.1007/s10703-022-00406-7
Cabodi GCamurati PPalena MPasini PVendraminetto D(2020)Reducing Interpolant Circuit Size Through SAT-Based WeakeningIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2019.291531739:7(1524-1531)Online publication date: 17-Jun-2020
https://dl.acm.org/doi/10.1109/TCAD.2019.2915317
Cabodi GCamurati PPalena MPasini PVendraminetto D(2019)Logic Synthesis for Interpolant Circuit CompactionIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2018.280822938:2(380-384)Online publication date: Feb-2019
https://doi.org/10.1109/TCAD.2018.2808229
Cabodi GCamurati PPalena MPasini PVendraminetto DPiskac RTalupur M(2016)Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakeningProceedings of the 16th Conference on Formal Methods in Computer-Aided Design10.5555/3077629.3077640(25-32)Online publication date: 3-Oct-2016
https://dl.acm.org/doi/10.5555/3077629.3077640
Cabodi GCamurati PPalena MPasini PVendraminetto D(2016)Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakening2016 Formal Methods in Computer-Aided Design (FMCAD)10.1109/FMCAD.2016.7886657(25-32)Online publication date: Oct-2016
https://doi.org/10.1109/FMCAD.2016.7886657
Cabodi GCamurati PFinocchiaro SLoiacono CSavarese FVendraminetto D(2016)Secure embedded architectures: Taint properties verification2016 International Conference on Development and Application Systems (DAS)10.1109/DAAS.2016.7492565(150-157)Online publication date: May-2016
https://doi.org/10.1109/DAAS.2016.7492565
Cabodi GLoiacono CVendraminetto D(2015)Optimization techniques for craig interpolant compaction in unbounded model checkingFormal Methods in System Design10.1007/s10703-015-0229-046:2(135-162)Online publication date: 1-Apr-2015
https://dl.acm.org/doi/10.1007/s10703-015-0229-0
Cabodi GPalena MPasini PJobstmann B(2014)Interpolation with Guided RefinementProceedings of the 14th Conference on Formal Methods in Computer-Aided Design10.5555/2682923.2682938(43-50)Online publication date: 21-Oct-2014
https://dl.acm.org/doi/10.5555/2682923.2682938
Cabodi GPalena MPasini P(2014)Interpolation with Guided Refinement: Revisiting incrementality in SAT-based unbounded model checking2014 Formal Methods in Computer-Aided Design (FMCAD)10.1109/FMCAD.2014.6987594(43-50)Online publication date: Oct-2014
https://doi.org/10.1109/FMCAD.2014.6987594
Cabodi GLoiacono CVendraminetto DMacii E(2013)Optimization techniques for craig interpolant compaction in unbounded model checkingProceedings of the Conference on Design, Automation and Test in Europe10.5555/2485288.2485625(1417-1422)Online publication date: 18-Mar-2013
https://dl.acm.org/doi/10.5555/2485288.2485625
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents