Techniques for verifying superscalar microprocessors

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Techniques for verifying superscalar microprocessors

Full text

Pdf (112 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: 552 - 557

Year of Publication: 1996

ISBN:0-89791-779-0

Author

Jerry R. Burch

Cadence Berkeley Laboratories

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): 27, 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/240518.240623 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	Daniel Brand, Verification of large synthesized designs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.534-537, November 07-11, 1993, Santa Clara, California, United States
	3	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
	4	A. J. Cohn. A proof of correctness of the Viper microprocessors: The first level. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 27-72. Kluwer, 1988.
	5	Francisco Corella , Michel Langevin , Eduard Cerny , Z. Zhou , Xiaoyu Song, State enumeration with abstract descriptions of state machines, Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.146-160, October 02-04, 1995
	6	D. Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, SRI Computer Science Laboratory, Dec. 1993.
	7	M. Damiani and G. D. Micheli. Observability don't care sets and boolean relations. In Intl. Conf. on Comp. Aided Design, 1990.
	8	David A. Patterson , John L. Hennessy, Computer architecture: a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1990
	9	W. A. Hunt, Jr. FM8501: A verified microprocessor. Technical Report 47, University of Texas at Austin, Institute for Computing Science, Dec. 1985.
	10	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
	11	Hamid Savoj , Robert K. Brayton, The use of observability and external don't cares for the simplification of multi-level networks, Proceedings of the 27th ACM/IEEE conference on Design automation, p.297-301, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123280]
	12	M. Srivas and S. P. Miller. Applying formal verification to a commercial microprocessor. In Computer Hardware Description Languages, Aug. 1995.
	13	Phillip J. Windley, Formal Modeling and Verification of Microprocessors, IEEE Transactions on Computers, v.44 n.1, p.54-72, January 1995 [doi>10.1109/12.368009]

CITED BY 25

	Randal E. Bryant , Steven German , Miroslav N. Velev, Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.93-134, Jan. 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
	Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors, Journal of Symbolic Computation, v.35 n.2, p.73-106, February 2003
	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
	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
	Robert B. Jones , Jens U. Skakkebæk , David L. Dill, Formal Verification of Out-of-Order Execution with Incremental Flushing, Formal Methods in System Design, v.20 n.2, p.139-158, March 2002
	Warren A. Hunt, Jr. , Jun Sawada, Verifying the FM9801 Microarchitecture, IEEE Micro, v.19 n.3, p.47-55, May 1999
	Miroslav N. Velev , Randal E. Bryant, Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction, Proceedings of the 37th conference on Design automation, p.112-117, June 05-09, 2000, Los Angeles, California, United States
	Randal E. Bryant , Miroslav N. Velev, Boolean satisfiability with transitivity constraints, ACM Transactions on Computational Logic (TOCL), v.3 n.4, p.604-627, October 2002
	Ravi Hosabettu , Ganesh Gopalakrishnan , Mandayam Srivas, A Practical Methodology for Verifying Pipelined Microarchitectures, IEEE Design & Test, v.20 n.04, p.4-14, January 2003
	Alberto L. Sangiovanni-Vincentelli , Patrick C. McGeer , Alexander Saldanha, Verification of electronic systems, Proceedings of the 33rd annual conference on Design automation, p.106-111, June 03-07, 1996, Las Vegas, Nevada, United States
	Miroslav N. Velev , Randal E. Bryant, Exploiting positive equality and partial non-consistency in the formal verification of pipelined microprocessors, Proceedings of the 36th ACM/IEEE conference on Design automation, p.397-401, June 21-25, 1999, New Orleans, Louisiana, United States
	Jun Sawada , Warren A. Hunt, Jr., Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability, Formal Methods in System Design, v.20 n.2, p.187-222, March 2002
	Miroslav N. Velev, Efficient formal verification of pipelined processors with instruction queues, Proceedings of the 14th ACM Great Lakes symposium on VLSI, April 26-28, 2004, Boston, MA, USA
	Miroslav N. Velev, Efficient translation of boolean formulas to CNF in formal verification of microprocessors, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.310-315, January 27-30, 2004, Yokohama, Japan
	Miroslav N. Velev, Using positive equality to prove liveness for pipelined microprocessors, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.316-321, January 27-30, 2004, Yokohama, Japan
	Miroslav N. Velev, Comparison of schemes for encoding unobservability in translation to SAT, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
	Roma Kane , Panagiotis Manolios , Sudarshan K. Srinivasan, Monolithic verification of deep pipelines with collapsed flushing, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
	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
	Miroslav N. Velev, Formal Verification of Pipelined Microprocessors with Delayed Branches, Proceedings of the 7th International Symposium on Quality Electronic Design, p.296-299, March 27-29, 2006
	Miroslav N. Velev, Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction, Proceedings of the 7th International Symposium on Quality Electronic Design, p.51-56, March 27-29, 2006
	Miroslav N. Velev, Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors, Proceedings of the conference on Design, automation and test in Europe, p.10266, February 16-20, 2004
	Nishant Sinha, Symbolic program analysis using term rewriting and generalization, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-9, November 17-20, 2008, Portland, Oregon
	S. Merniz , M. Benmohammed, Modelling and verification of superscalar Micro-architectures functional approach, Proceedings of the 12th WSEAS international conference on Computers, p.446-451, July 23-25, 2008, Heraklion, Greece