research-article

Analyzing k-step induction to compute invariants for SAT-based property checking

Authors:

Minh D. Nguyen,

Dominik Stoffel,

Wolfgang KunzAuthors Info & Claims

DAC '10: Proceedings of the 47th Design Automation Conference

Pages 176 - 181

https://doi.org/10.1145/1837274.1837319

Published: 13 June 2010 Publication History

Abstract

This paper proposes enhancements to SAT-based property checking with the goal to increase the spectrum of applications where a proof of unbounded validity of a safety property can be provided. For this purpose, invariants are computed by reachability analysis on an abstract model. The main idea of the paper consists in a BDD-based analysis of k-step-induction on the abstract model and its use to guide a step-wise refinement process of the initial abstraction. The property is then proven on a bounded model of the original design using the computed invariant. The new approach has been applied to formally verify industrial SoC modules. In our experiments, we consider particularly difficult verification tasks occurring in the context of protocol compliance verification using generic, transaction-style verification IPs. In our experiments, numerous properties are proven which either required substantial manual interaction in previous approaches, or cannot be proven at all by other methods available to us.

References

[1]

ABC. http://www.eecs.berkeley.edu/alanmi/abc/.

[2]

M. F. Ali, S. Safarpour, A. Veneris, M. S. Abadir, and R. Drechsler. Post-verification debugging of hierarchical designs. In Proc. International Conference on Computer-Aided Design (ICCAD), 2005.

Digital Library

[3]

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1999.

Digital Library

[4]

P. Bjesse and K. Claessen. SAT-based verification without state space traversal. In Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 372--389, 2000.

Digital Library

[5]

J. Bormann. Vollständige Verifikation. Dissertation, Technische Universität Kaiserslautern, 2009.

[6]

R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: A system for verification and synthesis. In R. Alur and T. Henzinger, editors, Proc. International Conference on Computer-Aided Verification (CAV), volume 1102, pages 428--432, New Brunswick, NJ, July 1996.

Digital Library

[7]

G. Cabodi, S. Nocco, and S. Quer. Improving SAT-based bounded model checking by means of BDD-based approximate traversals. Journal of Universal Computer Science, 10:1693--1730, 2004.

[8]

H. Cho, G. D. Hachtel, E. Macii, B. Plessier, and F. Somenzi:. Algorithms for approximate FSM traversal based on state space decomposition. IEEE Transactions on Computer-Aided Design, 15(12):1465--1478, December 1996.

Digital Library

[9]

H. Cho, G. D. Hachtel, E. Macii, M. Poncino, and F. Somenzi. Automatic state space decomposition for approximate FSM traversal based on circuit analysis. IEEE Transactions on Computer-Aided Design, 15(12):1451--1464, December 1996.

Digital Library

[10]

A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model verifier. In N. Halbwachs and D. Peled, editors, Proc. International Conference on Computer Aided Verification (CAV), number 1633 in Lecture Notes in Computer Science, pages 495--499, Trento, Italy, July 1999. Springer.

Digital Library

[11]

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, 50(5):752--794, 2003.

Digital Library

[12]

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Proc. International Conference on Computer Aided Verification (CAV), pages 154--169, 2000.

Digital Library

[13]

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, London, England, 1999.

Digital Library

[14]

N. Een and N. Soerensson. Temporal induction by incremental sat solving. In Proc. International Workshop on Bounded Model Checking (BMC03), 2003.

[15]

A. Gupta, M. Ganai, C. Wang, Z. Yang, and P. Ashar. Abstraction and BDDs complement SAT-based BMC in DiVer. In Proc. International Conference on Computer-Aided Design (ICCAD), 2003.

[16]

A. Gupta, M. Ganai, Z. Yang, and P. Ashar. Iterative abstraction using SAT-based BMC with proof analysis. In Proc. International Conference on Computer-Aided Design (ICCAD), page 416, Washington, DC, USA, 2003. IEEE Computer Society.

Digital Library

[17]

H. Jain, D. Kroening, N. Sharygina, and E. M. Clarke. Vcegar: Verilog counterexample guided abstraction refinement. In TACAS, pages 583--586, 2007.

Digital Library

[18]

K. L. McMillan. Interpolation and SAT-based model checking. In Proc. International Conference on Computer Aided Verification (CAV), 2003.

[19]

K. L. McMillan and N. Amla. Automatic abstraction without counterexamples. In Proc. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 2--17, 2003.

Digital Library

[20]

I.-H. Moon, J. Kakula, T. Shiple, and F. Somenzi. Least fixpoint approximations for reachability analysis. In Proc. International Conference on Computer-Aided Design (ICCAD), pages 41--44, 1999.

Digital Library

[21]

M. Nguyen, M. Thalmaier, M. Wedler, D. Stoffel, and W. Kunz. A re-use methodology for formal soc protocol compliance. In Proc. Forum on Specification & Design Languages(FDL), Sophia Antipolis, France, September 2009.

[22]

M. D. Nguyen, M. Thalmaier, M. Wedler, J. Bormann, D. Stoffel, and W. Kunz. Unbounded protocol compliance verification using interval property checking with invariants. IEEE Transactions on Computer-Aided Design, 27(11):2068--2082, November 2008.

Digital Library

[23]

Onespin Solutions GmbH, Germany. OneSpin 360MV.

[24]

M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a SAT-solver. In Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2000.

Digital Library

[25]

F. Somenzi. CUDD: CU Decision Diagram Package.

[26]

C. Wang, B. Li, H. Jin, G. D. Hachtel, and F. Somenzi. Improving ariadne's bundle by following multiple threads in abstraction refinement. In Proc. International Conference on Computer-Aided Design (ICCAD), 2002.

Digital Library

[27]

J. Yang and C.-J. H. Seger. Introduction to generalized symbolic trajectory evaluation. IEEE Transactions on VLSI Systems, 11(3):345--353, 2003.

Digital Library

Cited By

Yeh HWu CHuang C(2012)QuteRTLProceedings of the 18th international conference on Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-642-28756-5_26(377-391)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28756-5_26
Yeh HWu CHuang CPhillips JHu AGraeb H(2011)Property-specific sequential invariant extraction for SAT-based unbounded model checkingProceedings of the International Conference on Computer-Aided Design10.5555/2132325.2132475(674-678)Online publication date: 7-Nov-2011
https://dl.acm.org/doi/10.5555/2132325.2132475
Kahsai TGe YTinelli C(2011)Instantiation-based invariant discoveryProceedings of the Third international conference on NASA Formal methods10.5555/1986308.1986326(192-206)Online publication date: 18-Apr-2011
https://dl.acm.org/doi/10.5555/1986308.1986326

Index Terms

Analyzing k-step induction to compute invariants for SAT-based property checking
1. Hardware
  1. Hardware validation
    1. Functional verification

Recommendations

Property-specific sequential invariant extraction for SAT-based unbounded model checking
ICCAD '11: Proceedings of the International Conference on Computer-Aided Design

In this paper, we propose a property-specific sequential invariant extraction algorithm to improve the performance of the SAT-based Unbounded Modeling Checkers (UMCs). By analyzing the property-related predicates and their corresponding high-level ...
Evaluation of SAT-based Bounded Model Checking of ACTL Properties
TASE '07: Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering

Bounded model checking (BMC) based on SAT has been introduced as a complementary method to BDDbased symbolic model checking of LTL and ACTL properties in recent years. For general LTL and ACTL properties, BMC has traditionally aimed mainly at error ...
SAT-based unbounded symbolic model checking
DAC '03: Proceedings of the 40th annual Design Automation Conference

This paper describes a SAT-based unbounded symbolic model checking algorithm. BDDs have been widely used for symbolic model checking, but the approach suffers from memory overflow. The SAT procedure was exploited to overcome the problem, but it verified ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '10: Proceedings of the 47th Design Automation Conference

June 2010

1036 pages

ISBN:9781450300025

DOI:10.1145/1837274

General Chair:
Sachin Sapatnekar
Univ. of Minnesota, Minneapolis, MN

Copyright © 2010 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]

Sponsors

EDAC: Electronic Design Automation Consortium
SIGDA: ACM Special Interest Group on Design Automation
IEEE-CEDA

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 June 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

DAC '10

Sponsor:

EDAC
SIGDA

DAC '10: The 47th Annual Design Automation Conference 2010

June 13 - 18, 2010

California, Anaheim

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
161
Total Downloads

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

Reflects downloads up to 25 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yeh HWu CHuang C(2012)QuteRTLProceedings of the 18th international conference on Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-642-28756-5_26(377-391)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28756-5_26
Yeh HWu CHuang CPhillips JHu AGraeb H(2011)Property-specific sequential invariant extraction for SAT-based unbounded model checkingProceedings of the International Conference on Computer-Aided Design10.5555/2132325.2132475(674-678)Online publication date: 7-Nov-2011
https://dl.acm.org/doi/10.5555/2132325.2132475
Kahsai TGe YTinelli C(2011)Instantiation-based invariant discoveryProceedings of the Third international conference on NASA Formal methods10.5555/1986308.1986326(192-206)Online publication date: 18-Apr-2011
https://dl.acm.org/doi/10.5555/1986308.1986326

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents