skip to main content
10.1145/1118299.1118303acmconferencesArticle/Chapter ViewAbstractPublication PagesaspdacConference Proceedingsconference-collections
Article

Transition-based coverage estimation for symbolic model checking

Published: 24 January 2006 Publication History

Abstract

Lack of complete formal specification is one of the major obstacles for the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. It is more comprehensive and accurate than the existing coverage metrics for model checking. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.

References

[1]
E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.]]
[2]
Y. Hoskote, T. Kam, Pei-Hsin Ho, and Xudong Zhao. "Coverage estimation for symbolic model checking". In Proceedings of the 36th Design Automation Conference (DAC), page 300--305, 1999.]]
[3]
N. Jayakumar, M. Purandare, and F. Somenzi. "Do's and don'ts of CTL state coverage estimation". In Proceedings of the 40th Design Automation Conference (DAC), page 292--295, 2003.]]
[4]
X. Xu, S. Kimura, K. Horikawa, and T. Tsuchiya. "Transition Traversal Coverage Estimation for Symbolic Model Checking". In Proceedings of the 3rd ACM/IEEE international Confernece on Formal Methods and Models for Co-Design (MEMOCODE), page 259--260, 2005.]]
[5]
S. Katz, O., Grumberg, and D. Geist. "Have I written enough properties? - A method of comparison between specification and implementation". In Proceedings of the 10th ACM Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARM), page 280--297, 1999.]]
[6]
H. Chockler, O. Kupferman, and M. Y. Vardi. "Coverage Metrics for Formal Verification". In Proceedings of 12th ACM Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARM), page 111--125, 2003.]]
[7]
H. Chockler, O. Kupferman, R. Kurshan and M. Y. Vardi. "A Practical Approach to Coverage in Model Checking". In Proceedings of the 2001 International Conference on Computer Aided Verification (CAV), page 66--78, 2001.]]
[8]
F. Fummi, G. Pravadelli, A. Fedeli, U. Rossi, and F. Toto. "On the use of a high-level fault model to check properties incompleteness". In Proceedings of the 1st ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE), pages 145--152, 2003.]]
[9]
F. Wang, G.-D. Huang, F. Yu. "Numerical Coverage Estimation for the symbolic simulation of real-time systems". FORTE 2003, LNCS 2767, pages 160--176, 2003.]]
[10]
S. Tasiran, and K. Keutzer. "Coverage metrics for functional validation of hardware designs". In IEEE Journals of Design & Test of Computers, Volume 18(4), pages 36--45, 2001.]]
[11]
Y. Hoskote, D. Moundanos, and J. A. Abraham. "Automatic extraction of the control flow machine and application to evaluating coverage of verification vectors". In Proceedings of the 1995 IEEE Internatinal Conference on Computer Design VLSI in Computers and Processors (ICCD), page 532--537, 1995.]]
[12]
R. C. Ho, C. Han Yang, M. A. Horowitz, and D. L. Dill. "Architecture validation for processors". In Proceedings of the 22nd Annual International Symposium on Computer Architecture, page 404--413, 1995.]]
[13]
S. Das, et al. "Formal Verification Coverage: Computing the Coverage Gap between Temoral Specifications". In Proceedings of the IEEE/ACM International Conference on Compute Aided Design (ICCAD), page 198--203, 2004.]]
[14]
R. K. Brayton, et al. "VIS: A System for Verification and Synthesis". In Proceedings of the 1996 International Conference on Computer Aided Verification (CAV), page 428--432, 1996.]]
[15]
A. Gupta, S. Malik, and P. Ashar. "Toward Formalizing A Validation Methodology Using Simulation Coverage". In Proceedings of the 34th Design Automation Conference (DAC), page 740--745, 1997.]]
[16]
D. Chaiken, C. Fields, K. Kurihara, and A. Agarwal. "Directory-based cache coherence in large-scale multiprocessors Computer". In Computer, IEEE Computer Society, Volume 23, Issue 6, page 49--58, 1999.]]

Cited By

View all
  • (2016)An accurate algorithm for computing mutation coverage in model checking2016 IEEE International Test Conference (ITC)10.1109/TEST.2016.7805864(1-10)Online publication date: Nov-2016
  • (2014)Accelerating Coverage Estimation Through Partial Model CheckingIEEE Transactions on Computers10.1109/TC.2013.6363:7(1613-1625)Online publication date: Jul-2014
  • (2014)Optimization of the Translation of Labeled Transition Systems to Kripke StructuresProceedings of International Conference on Computer Science and Information Technology10.1007/978-81-322-1759-6_87(759-766)Online publication date: 2014
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ASP-DAC '06: Proceedings of the 2006 Asia and South Pacific Design Automation Conference
January 2006
998 pages
ISBN:0780394518

Sponsors

  • IEEE Circuits and Systems Society
  • SIGDA: ACM Special Interest Group on Design Automation
  • IEICE ESS: Institute of Electronics, Information and Communication Engineers, Engineering Sciences Society
  • IPSJ SIG-SLDM: Information Processing Society of Japan, SIG System LSI Design Methodology

Publisher

IEEE Press

Publication History

Published: 24 January 2006

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Acceptance Rates

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

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 17 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2016)An accurate algorithm for computing mutation coverage in model checking2016 IEEE International Test Conference (ITC)10.1109/TEST.2016.7805864(1-10)Online publication date: Nov-2016
  • (2014)Accelerating Coverage Estimation Through Partial Model CheckingIEEE Transactions on Computers10.1109/TC.2013.6363:7(1613-1625)Online publication date: Jul-2014
  • (2014)Optimization of the Translation of Labeled Transition Systems to Kripke StructuresProceedings of International Conference on Computer Science and Information Technology10.1007/978-81-322-1759-6_87(759-766)Online publication date: 2014
  • (2009)The role of mutation analysis for property qualificationProceedings of the 7th IEEE/ACM international conference on Formal Methods and Models for Codesign10.5555/1715759.1715763(28-35)Online publication date: 13-Jul-2009
  • (2009)The role of mutation analysis for property qualification2009 7th IEEE/ACM International Conference on Formal Methods and Models for Co-Design10.1109/MEMCOD.2009.5185375(28-35)Online publication date: Jul-2009
  • (2008)Reuse and optimization of testbenches and properties in a TLM-to-RTL design flowACM Transactions on Design Automation of Electronic Systems (TODAES)10.1145/1367045.136705613:3(1-22)Online publication date: 25-Jul-2008
  • (2007)Properties Incompleteness Evaluation by Functional VerificationIEEE Transactions on Computers10.1109/TC.2007.101256:4(528-544)Online publication date: 1-Apr-2007
  • (2007)Assignment coverage, a complementary coverage metric in formal verification2007 International Conference on Design & Technology of Integrated Systems in Nanoscale Era10.1109/DTIS.2007.4449496(76-81)Online publication date: Sep-2007
  • (2007)Too Few or Too Many Properties? Measure it by ATPG!Journal of Electronic Testing: Theory and Applications10.1007/s10836-007-5015-523:5(373-388)Online publication date: 1-Oct-2007

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media