Article

Automatic assume guarantee analysis for assertion-based formal verification

Authors:

Dong Wang,

Jeremy LevittAuthors Info & Claims

ASP-DAC '05: Proceedings of the 2005 Asia and South Pacific Design Automation Conference

Pages 561 - 566

https://doi.org/10.1145/1120725.1120963

Published: 18 January 2005 Publication History

Get Access

Abstract

Assertion based verification encourages the insertion of many assertions into a design. Typically, not all assertions can be proven (or falsified). The indeterminate assertions require manual analysis in order to determine design correctness -- a time-consuming and error-prone process. This paper shows how automatic assume guarantee reasoning can be used to reduce the amount of manual analysis. We present algorithms to automatically compute the assume guarantee relations between assertions. We extend circular assume guarantee reasoning to compute more proofs. And, we show how automatic assume guarantee reasoning can be used in practice to reduce the number of indeterminate assertions requiring manual analysis. We present the results of applying our algorithms to large industrial designs.

References

[1]

R. Alur, L. Alfaro, T. Henzinger, and F. Mang, "Automating modular verification," in CONCUR, 1999, pp. 82--97.]]

Digital Library

Google Scholar

[2]

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, "Symbolic model checking without BDDs," in TACAS, 1999.]]

Digital Library

Google Scholar

[3]

P. Chauhan, E. Clarke, S. Sapra, J. Kukula, H. Veith, and D. Wang, "Automated abstraction refinement for model checking large state spaces using sat based conflict analysis," in FMCAD, 2002.]]

Digital Library

Google Scholar

[4]

J. Cobleigh, D. Giannakopoulou, and C. Pasareanu, "Learning assumptions for compsotional verification," in TACAS, 2003.]]

Google Scholar

[5]

N. Een and N. Sorensson, "Temporal induction by incremental sat solving," in First International Workshop on Bounded Model Checking, 2003.]]

Google Scholar

[6]

A. Gupta, M. Ganai, P. Ashar, and Z. Yang, "Iterative abstraction using sat-based bmc with proof analysis," in ICCAD, 2003.]]

Digital Library

Google Scholar

[7]

T. Henzinger, S. Qadeer, and S. Rajamani, "You assume, we guarantee: methodology and case studies," in CAV, 1998, pp. 440--451.]]

Digital Library

Google Scholar

[8]

K. McMillan and N. Amla, "Automatic abstraction without counterexamples," in TACAS, 2003.]]

Google Scholar

[9]

K. L. McMillan, "Circular compositional reasonining about liveness," in CHARME, 1999.]]

Digital Library

Google Scholar

[10]

A. Pnueli, "In transition from global to modular temporal reasoning about programs," in Logic and Models of Concurrent Systems, 1984, pp. 123--144.]]

Digital Library

Google Scholar

[11]

M. Sheeran, S. Singh, and G. Stalmarck, "Checking safety properties using induction and a sat-solver," in FMCAD, 2000.]]

Digital Library

Google Scholar

[12]

D. Wang, P.-H. Ho, J. Long, J. Kukula, Y. Zhu, T. Ma, and R. Damiano, "Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines," in DAC, 2001.]]

Digital Library

Google Scholar

Cited By

View all

Tan SXiang DLu LLu JJiang QChen MYin JTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident VerificationProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651360(671-688)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651360
Pal DOffenberger SVasudevan S(2020)Assertion Ranking Using RTL Source Code AnalysisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2019.292137439:8(1711-1724)Online publication date: 1-Aug-2020
https://dl.acm.org/doi/10.1109/TCAD.2019.2921374
Todman TLuk W(2017)In-Circuit Assertions and Exceptions for Reconfigurable Hardware DesignProvably Correct Systems10.1007/978-3-319-48628-4_11(265-281)Online publication date: 2-Mar-2017
https://doi.org/10.1007/978-3-319-48628-4_11
Show More Cited By

Automatic assume guarantee analysis for assertion-based formal verification
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation

Recommendations

Automated circular assume-guarantee reasoning
Abstract
Model checking is a successful approach for verifying hardware and software systems. Despite its success, the technique suffers from the state explosion problem which arises due to the large state space of real-life systems. One solution to the ...
Reachability Assume-Guarantee
CTRQ '10: Proceedings of the 2010 Third International Conference on Communication Theory, Reliability, and Quality of Service

Model checking is a well known formal technique for systems verification and its main challenge is state explosion. Assume-guarantee is a promising way to deal with this challenge, but in the compositional reasoning process we should provide assumption ...
Symbolic assume-guarantee reasoning through BDD learning
ICSE 2014: Proceedings of the 36th International Conference on Software Engineering

Both symbolic model checking and assume-guarantee reasoning aim to circumvent the state explosion problem. Symbolic model checking explores many states simultaneously and reports numerous erroneous traces. Automated assume-guarantee reasoning, on the ...

Comments

Information & Contributors

Information

Published In

ASP-DAC '05: Proceedings of the 2005 Asia and South Pacific Design Automation Conference

January 2005

1495 pages

ISBN:0780387376

DOI:10.1145/1120725

General Chair:
Ting-Ao Tang
Fudan University, Shanghai, P. R. China

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

Publication History

Published: 18 January 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ASPDAC05

Sponsor:

SIGDA

ASPDAC05: Asia and South Pacific Design Automation Conference

January 18 - 21, 2005

Shanghai, China

Acceptance Rates

Overall Acceptance Rate 466 of 1,454 submissions, 32%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
181
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Tan SXiang DLu LLu JJiang QChen MYin JTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident VerificationProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651360(671-688)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651360
Pal DOffenberger SVasudevan S(2020)Assertion Ranking Using RTL Source Code AnalysisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2019.292137439:8(1711-1724)Online publication date: 1-Aug-2020
https://dl.acm.org/doi/10.1109/TCAD.2019.2921374
Todman TLuk W(2017)In-Circuit Assertions and Exceptions for Reconfigurable Hardware DesignProvably Correct Systems10.1007/978-3-319-48628-4_11(265-281)Online publication date: 2-Mar-2017
https://doi.org/10.1007/978-3-319-48628-4_11
Hertz SSheridan DVasudevan S(2013)Mining Hardware Assertions With Guidance From Static AnalysisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2013.224117632:6(952-965)Online publication date: 1-Jun-2013
https://dl.acm.org/doi/10.1109/TCAD.2013.2241176
Arnaout TBartsch GWunderlich H(2006)Some Common Aspects of Design Validation,Debug and DiagnosisProceedings of the Third IEEE International Workshop on Electronic Design, Test and Applications10.1109/DELTA.2006.79(3-10)Online publication date: 17-Jan-2006
https://dl.acm.org/doi/10.1109/DELTA.2006.79

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.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Recommendations

Automated circular assume-guarantee reasoning

Reachability Assume-Guarantee

Symbolic assume-guarantee reasoning through BDD learning

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations