Efficient validity checking for processor verification

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Efficient validity checking for processor verification

Full text

Publisher Site , Pdf

Pdf (88 KB)

Source

International Conference on Computer Aided Design archive
Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design table of contents

San Jose, California, United States

Pages: 2 - 6

Year of Publication: 1995

ISBN:0-8186-7213-7

Authors

Robert B. Jones	Computer Systems Laboratory, Stanford University, Stanford, CA
David L. Dill	Computer Systems Laboratory, Stanford University, Stanford, CA
Jerry R. Burch	Cadence Berkeley Laboratories, Berkeley, CA

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS : Computer Society

Publisher

IEEE Computer Society Washington, DC, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 20, Citation Count: 13

Additional Information:

abstract references cited by index terms collaborative colleagues peer to peer

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

ABSTRACT

We describe an efficient validity checker for the quantifier-free logic of equality with uninterpreted functions. This logic is well suited for verifying microprocessor control circuitry since it allows the abstraction of datapath values and operations. Our validity checker uses special data structures to speed up case splitting, and powerful heuristics to reduce the number of case splits needed. In addition, we present experimental results and show that this implementation has enabled the automatic verification of an actual high-level microprocessor description.

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.

	BD94a	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]
	BD94b	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
	Bea93	Derek Lee Beatty, A methodology for formal hardware verification, with application to microprocessors, Carnegie Mellon University, Pittsburgh, PA, 1993
	C+94	F. Corella et al. Multiway decision graphs for automated hardware verification. Unpublished manuscript, August 1994.
	CLR90	Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
	Cyr93	D. Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, SRI Computer Science Laboratory, December 1993.
	HP90	David A. Patterson , John L. Hennessy, Computer architecture: a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1990
	K+94	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
	LCDM89	E Lammens, L. Claesen, and H. De Man. Correctness verification of VLSI modules supported by a very efficient boolean prover. In Proceedings: IEEE International Conference on Computer Design, October 1989.
	Nel81	G. Nelson. Techniques for program verification. Technical Report CSL-81-10, Xerox PARC, June 1981.
	NO79	Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
	NO80	Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
	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]
	Sho79	Robert E. Shostak, A Practical Decision Procedure for Arithmetic with Function Symbols, Journal of the ACM (JACM), v.26 n.2, p.351-360, April 1979 [doi>10.1145/322123.322137]
	SM95	M. Srivas and S. P. Miller. Applying formal verification to a commercial microprocessor. In Computer Hardware Description Languages, August 1995.
	Tar75	Robert Endre Tarjan, Efficiency of a Good But Not Linear Set Union Algorithm, Journal of the ACM (JACM), v.22 n.2, p.215-225, April 1975 [doi>10.1145/321879.321884]
	Wil95	R. Wilson. Verification feels strain. Electronic Engineering Times, (840): 18-22, March 1995.
	Win95	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 13

	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
	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
	Clark W. Barrett , David L. Dill , Jeremy R. Levitt, A decision procedure for bit-vector arithmetic, Proceedings of the 35th annual conference on Design automation, p.522-527, June 15-19, 1998, San Francisco, California, United States
	Jerry R. Burch, Techniques for verifying superscalar microprocessors, Proceedings of the 33rd annual conference on Design automation, p.552-557, June 03-07, 1996, Las Vegas, Nevada, United States
	Pranav Ashar , Subhrajit Bhattacharya , Anand Raghunathan , Akira Mukaiyama, Verification of RTL generated from scheduled behavior in a high-level synthesis flow, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.517-524, November 08-12, 1998, San Jose, California, 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
	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
	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
	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
	Anuj Goel , Khurram Sajid , Hai Zhou , Adnan Aziz , Vigyan Singhal, BDD Based Procedures for a Theory of Equality with Uninterpreted Functions, Formal Methods in System Design, v.22 n.3, p.205-224, May 2003
	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, 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
	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