A scalable formal verification methodology for pipelined microprocessors

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A scalable formal verification methodology for pipelined microprocessors

Full text

Pdf (135 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 33rd annual Design Automation Conference table of contents

Las Vegas, Nevada, United States

Pages: 558 - 563

Year of Publication: 1996

ISBN:0-89791-779-0

Authors

Jeremy Levitt	Computer Systems Laboratory, Stanford University, CA
Kunle Olukotun	Computer Systems Laboratory, Stanford University, CA

Sponsors

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

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 11, Citation Count: 5

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/240518.240624 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	Vishal Bhagwati , Srinivas Devadas, Automatic verification of pipelined microprocessors, Proceedings of the 31st annual conference on Design automation, p.603-608, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196577]
	2	Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
	3	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]
	4	A.J. Cohn, "A Proof of Correctness of the Viper Microprocessor: The First Level," in VLSI Specification, Verification and Synthesis, G. Birtwistle and E A. Subrahmanyam, editors, pp. 27-72. Kluwer Academic Publishers, 1988.
	5	David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
	6	M. J. C. Gordon, "HOL: A proof generation system for higher-order logic," in VLSI Specification, Verification and Synthesis, G. Birtwistle and E A. Subrahmanyam, editors, pp. 73-120. Kluwer Academic publishers, Boston, MA, 1988
	7	John L. Hennessy , David A. Patterson, Computer architecture (2nd ed.): a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
	8	Robert B. Jones , David L. Dill , Jerry R. Burch, Efficient validity checking for processor verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.2-6, November 05-09, 1995, San Jose, California, United States
	9	M. C. McFarland, "Formal Verification of Sequential Hardware: A Tutorial," IEEE Transactions on computer-Aided Design of Integrated Circuits and Systems, vol. 12, no. 5, May 1993.
	10	K. L. McMillan, Fitting formal methods into the design cycle, Proceedings of the 31st annual conference on Design automation, p.314-319, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196392]
	11	Mandayam Srivas , Mark Bickford, Formal Verification of a Pipelined Microprocessor, IEEE Software, v.7 n.5, p.52-64, September 1990 [doi>10.1109/52.57892]

CITED BY 5

	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
	Jeremy Levitt , Kunle Olukotun, Verifying correct pipeline implementation for microprocessors, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.162-169, November 09-13, 1997, San Jose, California, United States
	James K. Huggins , David Van Campenhout, Specification and verification of pipelining in the ARM2 RISC microprocessor, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.3 n.4, p.563-580, Oct. 1998
	Daniel Kroening , Wolfgang J. Paul, Automated pipeline design, Proceedings of the 38th conference on Design automation, p.810-815, June 2001, Las Vegas, Nevada, United States
	Aarti Gupta , Sharad Malik , Pranav Ashar, Toward formalizing a validation methodology using simulation coverage, Proceedings of the 34th annual conference on Design automation, p.740-745, June 09-13, 1997, Anaheim, California, United States