Automatic verification of pipelined microprocessors

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Automatic verification of pipelined microprocessors

Full text

Pdf (62 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 31st annual Design Automation Conference table of contents

San Diego, California, United States

Pages: 603 - 608

Year of Publication: 1994

ISBN:0-89791-653-0

Authors

Vishal Bhagwati	Research Laboratory of Electronics, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA
Srinivas Devadas	Research Laboratory of Electronics, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA

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): 3, Downloads (12 Months): 7, Citation Count: 10

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/196244.196577 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.

	AAD91	Filip Van Aelten , Stan Y. Liao , Jonathan Allen , Srinivas Devadas, Automatic generation and verification of sufficient correctness properties for synchronous processors, Proceedings of the 1992 IEEE/ACM international conference on Computer-aided design, p.183-187, November 1992, Santa Clara, California, United States
	Bhag93	V. Bhagwati. Automatic Verification of Pipelined Microprocessors. S.M. Thesis, MIT, 1993.
	BK89	S. Bose, and A. Fisher. Verifying pipelined hardware using symbolic logic simulation. In Proceedings of the IEEE Conference on Computer Design, pages 217-221, 1989.
	Bro89	Alexandre Bronstein, MLP: string-functional semantics and Boyer-Moore mechanization for the formal verification of synchronous circuits, Stanford University, Stanford, CA, 1990
	Bry86	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]
	Coh88	A. Cohn. A Proof of Correctness of the VIPER Microprocessor: The First Level. In G. Birtwistle and EA. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 111-128. Kluwer Academic Publishers, 1988.
	Cor93	Francisco Corella, Automated High-level Verification Against Clocked Algorithmic Specifications, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.147-154, April 26-28, 1993
	CBM89	O. Coudert, C. Berthet, and J.C. Madre. Verification of Sequential Machines Using Boolean Functional Vectors. In IMEC-IFIP Int'l Workshop on Applied Formal Methods for Correct VLSI Design, pages 111-128, November 1989.
	PH90	David A. Patterson , John L. Hennessy, Computer architecture: a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1990
	Hun85	W. Hunt, FM8501: A Verified Microprocessor. University of Texas, Austin, Tech. Report 47, 1985.
	Joy88	J. Joyce. Formal Verification and Implementation of a Microprocessor. In G. Birtwistle and EA. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 129- 157. Kluwer Academic Publishers, 1988.
	Koh78	Z. Kohavi. Switching and Finite Automata Theory. McGraw Hill, 1978.
	LC91	M. Langevin and E. Cerny. Verification of processor-like circuits. In E Printetto and E Camurati, editors, Advanced Research Workshop on Correct Hardware Design Methodologies, June 1991.
	Ros92	A.W. Roscoe. Occam in the specification and verification of microprocessors. Philosophical Transactions of the Royal Society of London, Series A: Physical Sciences and Engineering, 339(1652):137-151, Apr. 15, 1992.
	Seg87	R. Segal. BDSYN: Logic Description Translator. UC Berkeley, UCB ERL Memo No. M87/33, May 1987.
	SSM92	Ellen Sentovich , Kanwar Jit Singh , Cho W. Moon , Hamid Savoj , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Sequential Circuit Design Using Synthesis and Optimization, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.328-333, October 11-14, 1992
	SB90	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 10

	Richard C. Ho , C. Han Yang , Mark A. Horowitz , David L. Dill, Architecture validation for processors, ACM SIGARCH Computer Architecture News, v.23 n.2, p.404-413, May 1995
	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
	Hiroaki Iwashita , Satoshi Kowatari , Tsuneo Nakata , Fumiyasu Hirose, Automatic test program generation for pipelined processors, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.580-583, November 06-10, 1994, San Jose, California, United States
	David Van Campenhout , Trevor Mudge , John P. Hayes, High-level test generation for design verification of pipelined microprocessors, Proceedings of the 36th ACM/IEEE conference on Design automation, p.185-188, June 21-25, 1999, New Orleans, Louisiana, United States
	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
	Jeremy Levitt , Kunle Olukotun, A scalable formal verification methodology for pipelined microprocessors, Proceedings of the 33rd annual conference on Design automation, p.558-563, June 03-07, 1996, Las Vegas, Nevada, United States
	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
	Jian Shen , Jacob A. Abraham, An RTL Abstraction Technique for Processor MicroarchitectureValidation and Test Generation, Journal of Electronic Testing: Theory and Applications, v.16 n.1-2, p.67-81, Feb/April 2000
	Sofiéne Tahar , Ramayya Kumar, A Practical Methodology for the Formal Verification of RISC Processors, Formal Methods in System Design, v.13 n.2, p.159-225, Sept. 1998
	Anupam Chattopadhyay , Arnab Sinha , Diandian Zhang , Rainer Leupers , Gerd Ascheid , Heinrich Meyr, Integrated verification approach during ADL-driven processor design, Microelectronics Journal, v.40 n.7, p.1111-1123, July, 2009