Formally verifying a microprocessor using a simulation methodology

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Formally verifying a microprocessor using a simulation methodology

Full text

Pdf (93 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: 596 - 602

Year of Publication: 1994

ISBN:0-89791-653-0

Authors

Derek L. Beatty	Cadence Berkeley Laboratories, Cadence Design Systems, Inc.
Randal E. Bryant	Carnegie Mellon University

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): 1, Downloads (12 Months): 13, Citation Count: 22

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.196575 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	Derek Lee Beatty, A methodology for formal hardware verification, with application to microprocessors, Carnegie Mellon University, Pittsburgh, PA, 1993
	2	Derek L. Beatty , Randal E. Bryant , Carl-Johan H. Seger, Synchronous circuit verification by symbolic simulation: an illustration, Proceedings of the sixth MIT conference on Advanced research in VLSI, p.98-112, March 1990, Boston, Massachusetts, United States
	3	Randal E. Bryant , Derek L. Beatty , Carl-Johan H. Seger, Formal hardware verification by symbolic ternary trajectory evaluation, Proceedings of the 28th conference on ACM/IEEE design automation, p.397-402, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127701]
	4	A. Cohn. Correctness properties of the Viper block model: the second level. Technical report 134. University of Cambridge Comp. Lab., May 1988.
	5	Kenneth W. Fernald , Todd A. Cook , Thomas K. Miller, III , John J. Paulos, A Microprocessor-Based Implantable Telemetry System, Computer, v.24 n.3, p.23-30, March 1991 [doi>10.1109/2.73510]
	6	Warren Alva Hunt, Jr., Fm8501: a verified microprocessor (theorem-proving, computers, design), 1985
	7	J. J. Joyce. Multi Level Verification of Microprocessor-Based Systems. PhD thesis, published as technical report 195. Univ. of Cambridge, Comp. Lab., May 1990.
	8	Jean-Christophe Madre , Jean-Paul Billon, Proving circuit correctness using formal comparison between expected and extracted behaviour, Proceedings of the 25th ACM/IEEE conference on Design automation, p.205-210, June 12-15, 1988, Atlantic City, New Jersey, United States
	9	J.-C. Madre, O. Coudert, M. Currat, A. Debreil, and C. Berthet. The formal verification chain at BULL. EURO ASIC (Paris, 28 May- 1 June 1990), pages 474-9. IEEE, 1990.
	10	T.K. MillerIII, B. L. Bhuva, R. L. Barnes, J.-C. Dub, H.-B. Lin, and D. E. Van denBout. The HECTOR microprocessor. ICCD, pages 406-11, 1986.
	11	John Denniston Oakley, Symbolic execution of formal machine descriptions, 1979
	12	Carl J Seger , Bryant, R , E. al, Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories, University of British Columbia, Vancouver, BC, Canada, 1993
	13	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 22

	Samir Jain , Randal E. Bryant , Alok Jain, Automatic clock abstraction from sequential circuits, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.707-711, June 12-16, 1995, San Francisco, California, United States
	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
	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
	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
	Jin Yang , Amit Goel, GSTE through a case study, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.534-541, November 10-14, 2002, San Jose, California
	Kyle L. Nelson , Alok Jain , Randal E. Bryant, Formal verification of a superscalar execution unit, Proceedings of the 34th annual conference on Design automation, p.161-166, June 09-13, 1997, Anaheim, California, United States
	Jin Yang , Carl-Johan H. Seger, Introduction to generalized symbolic trajectory evaluation, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.11 n.3, p.345-353, June 2003
	Manish Pandey , Richard Raimi , Derek L. Beatty , Randal E. Bryant, Formal verification of PowerPC arrays using symbolic trajectory evaluation, Proceedings of the 33rd annual conference on Design automation, p.649-654, June 03-07, 1996, Las Vegas, Nevada, United States
	Narayanan Krishnamurthy , Magdy S. Abadir , Andrew K. Martin , Jacob A. Abraham, Design and Development Paradigm for Industrial Formal Verification CAD Tools, IEEE Design & Test, v.18 n.4, p.26-35, July 2001
	Ilan Beer , Shoham Ben-David , Cindy Eisner , Yoav Rodeh, Efficient Detection of Vacuity in Temporal Model Checking, Formal Methods in System Design, v.18 n.2, p.141-163, March 1, 2001
	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
	Alfred Kölbi , James Kukula , Kurt Antreich , Robert Damiano, Handling special constructs in symbolic simulation, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	Noppanunt Utamaphethai , R. D. Shawn Blanton , John Paul Shen, Effectiveness of Microarchitecture Test Program Generation, IEEE Design & Test, v.17 n.4, p.38-49, October 2000
	Jayanta Bhadra , Andrew K. Martin , Jacob A. Abraham, A formal framework for verification of embedded custom memories of the Motorola MPC7450 microprocessor, Formal Methods in System Design, v.27 n.1/2, p.67-112, September 2005
	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
	Noppanunt Utamaphethai , R. D. (Shawn) Blanton , John Paul Shen, A Buffer-Oriented Methodology for Microarchitecture Validation, Journal of Electronic Testing: Theory and Applications, v.16 n.1-2, p.49-65, Feb/April 2000
	I. Gibson , C. Amies, Practical concurrent ASIC and system design and verification, Proceedings of the 1997 European conference on Design and Test, p.532, March 17-20, 1997
	Guoqiang Pan , Moshe Y. Vardi, Symbolic Techniques in Satisfiability Solving, Journal of Automated Reasoning, v.35 n.1-3, p.25-50, October 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
	Hana Chockler , Ofer Strichman, Before and after vacuity, Formal Methods in System Design, v.34 n.1, p.37-58, February 2009
	Hana Chockler , Arie Gurfinkel , Ofer Strichman, Beyond vacuity: towards the strongest passing formula, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-8, November 17-20, 2008, Portland, Oregon
	Daniel Grosse , Robert Wille , Ulrich Kuehne , Rolf Drechsler, Contradictory antecedent debugging in bounded model checking, Proceedings of the 19th ACM Great Lakes symposium on VLSI, May 10-12, 2009, Boston Area, MA, USA