Coverage estimation for symbolic model checking

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Coverage estimation for symbolic model checking

Full text

Pdf (79 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 36th annual ACM/IEEE Design Automation Conference table of contents

New Orleans, Louisiana, United States

Pages: 300 - 305

Year of Publication: 1999

ISBN:1-58133-109-7

Authors

Yatin Hoskote	Strategic CAD Labs, Design Technology, Intel Corp.
Timothy Kam	Strategic CAD Labs, Design Technology, Intel Corp.
Pei-Hsin Ho	Advanced Technology Group, Synopsys, Inc.
Xudong Zhao	Strategic CAD Labs, Design Technology, Intel Corp.

Sponsors

EDAC : Electronic Design Automation Consortium
IEEE-CAS : Circuits & Systems
SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 15, Citation Count: 25

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/309847.309936 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	2	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	3	Kwang Ting Cheng , A. S. Krishnakumar, Automatic functional test generation using the extended finite state machine model, Proceedings of the 30th international conference on Design automation, p.86-91, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164585]
	4	Richard C. Ho , C. Han Yang , Mark A. Horowitz , David L. Dill, Architecture validation for processors, Proceedings of the 22nd annual international symposium on Computer architecture, p.404-413, June 22-24, 1995, S. Margherita Ligure, Italy
	5	Yatin V. Hoskote , Dinos Moundanos , Jacob A. Abraham, Automatic extraction of the control flow machine and application to evaluating coverage of verification vectors, Proceedings of the 1995 International Conference on Computer Design: VLSI in Computers and Processors, p.532-537, October 02-04, 1995
	6	Michael Katrowitz , Lisa M. Noack, I'm done simulating; now what? Verification coverage analysis and correctness checking of the DEC chip 21164 Alpha microprocessor, Proceedings of the 33rd annual conference on Design automation, p.325-330, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240580]
	7	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	8	H. Cho, G. Hachtel, F. Somenzi, "Redundancy Identification and Test Generation for Sequential Circuits Using Implicit State Enumeration," IEEE Transactions on CAD, vol 12, no. 7, pp. 935-945, 1993
	9	Pei-Hsin Ho , Adrian J. Isles , Timothy Kam, Formal verification of pipeline control using controlled token nets and abstract interpretation, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.529-536, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289082]

CITED BY 25

	Nikhil Jayakumar , Mitra Purandare , Fabio Somenzi, Dos and don'ts of CTL state coverage estimation, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
	Jin Yang , Avi Puder, Tightly integrate dynamic verification with formal verification: a GSTE based approach, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
	Bijan Alizadeh, Word level functional coverage computation, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan
	Görschwin Fey , Rolf Drechsler, Improving simulation-based verification by means of formal methods, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.640-643, January 27-30, 2004, Yokohama, Japan
	Xingwen Xu , Shinji Kimura , Kazunari Horikawa , Takehiko Tsuchiya, Transition-based coverage estimation for symbolic model checking, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan
	Serdar Tasiran , Kurt Keutzer, Coverage Metrics for Functional Validation of Hardware Designs, IEEE Design & Test, v.18 n.4, p.36-45, July 2001
	Jeremy S. Bradbury , James R. Cordy , Juergen Dingel, An empirical framework for comparing effectiveness of testing and property-based formal analysis, ACM SIGSOFT Software Engineering Notes, v.31 n.1, January 2006
	Franco Fummi , Graziano Pravadelli, Too Few or Too Many Properties? Measure it by ATPG!, Journal of Electronic Testing: Theory and Applications, v.23 n.5, p.373-388, October 2007
	Hana Chockler , Orna Kupferman , Moshe Y. Vardi, Coverage metrics for temporal logic model checking, Formal Methods in System Design, v.28 n.3, p.189-212, May 2006
	Shireesh Verma , Ian G. Harris , Kiran Ramineni, Interactive presentation: Automatic generation of functional coverage models from behavioral verilog descriptions, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
	Daniel Große , Ulrich Kühne , Rolf Drechsler, Estimating functional coverage in bounded model checking, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
	Bhaskar Pal , Ansuman Banerjee , Pallab Dasgupta , P. P. Chakrabarti, BUSpec: A framework for generation of verification aids for standard bus protocol specifications, Integration, the VLSI Journal, v.40 n.3, p.285-304, April, 2007
	Nicola Bombieri , Franco Fummi , Graziano Pravadelli, Incremental ABV for functional validation of TL-to-RTL design refinement, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
	Sanjit A. Seshia , Wenchao Li , Subhasish Mitra, Verification-guided soft error resilience, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
	A. Das , P. Basu , A. Banerjee , P. Dasgupta , P. P. Chakrabarti , C. Rama Mohan , L. Fix , R. Armoni, Formal verification coverage: computing the coverage gap between temporal specifications, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.198-203, November 07-11, 2004
	Aarti Gupta , Albert E. Casavant , Pranav Ashar , Akira Mukaiyama , Kazutoshi Wakabayashi , X. G. (Sean) Liu, Property-Specific Testbench Generation for Guided Simulation, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.524, January 07-11, 2002
	M. Borgatti , A. Capello , U. Rossi , J.-L. Lambert , I. Moussa , F. Fummi , G. Pravadelli, An Integrated Design and Verification Methodology for Reconfigurable Multimedia Systems, Proceedings of the conference on Design, Automation and Test in Europe, p.266-271, March 07-11, 2005
	Hana Chockler , Joseph Y. Halpern , Orna Kupferman, What causes a system to satisfy a specification?, ACM Transactions on Computational Logic (TOCL), v.9 n.3, p.1-26, June 2008
	Nicola Bombieri , Franco Fummi , Graziano Pravadelli, Reuse and optimization of testbenches and properties in a TLM-to-RTL design flow, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.3, p.1-22, July 2008
	Mahmoud Askari , Hamid Shojaei , Fataneh Faghani, Symbolic counter-example generation for model checking, Proceedings of the 7th WSEAS International Conference on Application of Electrical Engineering, p.154-159, July 02-04, 2008, Trondheim, Norway
	Yves Le Traon , Benoit Baudry , Jean-Marc Jezequel, Design by Contract to Improve Software Vigilance, IEEE Transactions on Software Engineering, v.32 n.8, p.571-586, August 2006
	Andrea Fedeli , Franco Fummi , Graziano Pravadelli, Properties Incompleteness Evaluation by Functional Verification, IEEE Transactions on Computers, v.56 n.4, p.528-544, April 2007
	Orna Kupferman , Wenchao Li , Sanjit A. Seshia, A theory of mutations with applications to vacuity, coverage, and fault tolerance, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-9, November 17-20, 2008, Portland, Oregon
	Hana Chockler , Ofer Strichman, Before and after vacuity, Formal Methods in System Design, v.34 n.1, p.37-58, February 2009
	Arnab Sinha , Pallab Dasgupta , Bhaskar Pal , Sayantan Das , Prasenjit Basu , P. P. Chakrabarti, Design intent coverage revisited, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.14 n.1, p.1-32, January 2009