Deriving a simulation input generator and a coverage metric from a formal specification

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Deriving a simulation input generator and a coverage metric from a formal specification

Full text

Pdf (92 KB)

Source

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

New Orleans, Louisiana, USA

SESSION: Moving towards more effective validation table of contents

Pages: 801 - 806

Year of Publication: 2002

ISBN ~ ISSN:0738-100X , 1-58113-461-4

Authors

Kanna Shimizu	Stanford University, Stanford, CA
David L. Dill	Stanford University, Stanford, CA

Sponsor

SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 18, Citation Count: 16

Additional Information:

abstract 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/513918.514118 What is a DOI?

ABSTRACT

This paper presents novel uses of functional interface specifications for verifying RTL designs. We demonstrate how a simulation environment, a correctness checker, and a functional coverage metric are all created automatically from a single specification. Additionally, the process exploits the structure of a specification written with simple style rules. The methodology was used to verify a large-scale I/O design from the Stanford FLASH project.

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	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]
	2	Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
	3	Edmund M. Clarke , Steven M. German , Yuan Lu , Helmut Veith , Dong Wang, Executable Protocol Specification in ESL, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.197-216, November 01-03, 2000
	4	Shankar G. Govindaraju , David L. Dill, Counterexample-guided choice of projections in approximate symbolic model checking, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
	5	J. Kuskin , D. Ofelt , M. Heinrich , J. Heinlein , R. Simoni , K. Gharachorloo , J. Chapin , D. Nakahira , J. Baxter , M. Horowitz , A. Gupta , M. Rosenblum , J. Hennessy, The Stanford FLASH multiprocessor, Proceedings of the 21ST annual international symposium on Computer architecture, p.302-313, April 18-21, 1994, Chicago, Illinois, United States
	6	K. McMillan. http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/
	7	OCAML. http://caml.inria.fr
	8	Kanna Shimizu , David L. Dill , Ching-Tsun Chou, A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® ItaniumTM Processor Bus Protocol, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.340-354, September 04-07, 2001
	9	Kanna Shimizu , David L. Dill , Alan J. Hu, Monitor-Based Formal Specification of PCI, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.335-353, November 01-03, 2000
	10	F. Somenzi. http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html
	11	Jun Yuan , Kurt Shultz , Carl Pixley , Hillel Miller , Adnan Aziz, Modeling design constraints and biasing in simulation using BDDs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.584-590, November 07-11, 1999, San Jose, California, United States

CITED BY 16

	Serdar Tasiran , Yuan Yu , Brannon Batson, Using a formal specification and a model checker to monitor and direct simulation, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
	Jun Yuan , Ken Albin , Adnan Aziz , Carl Pixley, Constraint synthesis for environment modeling in functional verification, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
	Annette Bunker , Ganesh Gopalakrishnan , Sally A. Mckee, Formal hardware specification languages for protocol compliance verification, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.9 n.1, p.1-32, January 2004
	Young-Su Kwon , Young-Il Kim , Chong-Min Kyung, Systematic functional coverage metric synthesis from hierarchical temporal event relation graph, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
	Serdar Tasiran , Yuan Yu , Brannon Batson, Linking Simulation with Formal Verification at a Higher Level, IEEE Design & Test, v.21 n.6, p.472-482, November 2004
	Ed Cerny , Ashvin Dsouza , Kevin Harer , Pei-Hsin Ho , Tony Ma, Supporting sequential assumptions in hybrid verification, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
	Ansuman Banerjee , Bhaskar Pal , Sayantan Das , Abhijeet Kumar , Pallab Dasgupta, Test generation games from formal specifications, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
	Nathan Kitchen , Andreas Kuehlmann, Stimulus generation for constrained random simulation, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
	Jun Yuan , Carl Pixley , Adnan Aziz , Ken Albin, A Framework for Constrained Functional Verification, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.142, November 09-13, 2003
	Smitha Shyam , Valeria Bertacco, Distance-guided hybrid verification with GUIDO, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
	Alessandro Pinto , Alvise Bonivento , Allberto L. Sangiovanni-Vincentelli , Roberto Passerone , Marco Sgroi, System level design paradigms: Platform-based design and communication synthesis, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.11 n.3, p.537-563, July 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
	Yunshan Zhu , James H. Kukula, Generator-based Verification, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.146, November 09-13, 2003
	Jayanta Bhadra , Magdy S. Abadir , Li-C. Wang , Sandip Ray, A Survey of Hybrid Techniques for Functional Verification, IEEE Design & Test, v.24 n.2, p.112-122, March 2007
	Namrata Shekhar , Priyank Kalla , M. Brandon Meredith , Florian Enescu, Simulation bounds for equivalence verification of polynomial datapaths using finite ring algebra, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.16 n.4, p.376-387, April 2008
	Yann Oddos , Katell Morin-Allory , Dominique Borrione , Marc Boulé , Zeljko Zilic, MYGEN: automata-based on-line test generator for assertion-based verification, Proceedings of the 19th ACM Great Lakes symposium on VLSI, May 10-12, 2009, Boston Area, MA, USA