Scalable hybrid verification of complex microprocessors

ABSTRACT

We introduce a new verification methodology for modern micro-processors that uses a simple checker processor to validate the exe-cution of a companion high-performance processor. The checker can be viewed as an at-speed emulator that is formally verified to be compliant to an ISA specification. This verification approach en-ables the practical deployment of formal methods without impact-ing overall performance.

REFERENCES

• 1: W. Ackermann,"Solvable Cases of the Decision Problem," Noth-Holland, Amsterdam, 1954.
• 2: F. A. Aloul and K. A. Sakallah, "Efficient Verification of the PCI Local Bus using Boolean Satisfiability," in IWLS,2000.
• 3: "Alpha Architecture Handbook," Product #EC-QD2KC-TE, Compaq Computer Corporation,1998.
• 4: T. Austin, "DIVA: A Dynamic Approach to Microprocessor Verification," in Journal of Instruction-Level Parallelism, Vol. 2, 2000.
• 5: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, Validity Checking for Combinations of Theories with Equality, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.187-201, November 06-08, 1996
• 6: R. Bryant, S. German, and M. Velev, "Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic," TR CMU-CS-99-115, 1999.
• 7: 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
• 8: Saugata Chatterjee , Chris Weaver , Todd Austin, Efficient checker processor design, Proceedings of the 33rd annual ACM/IEEE international symposium on Microarchitecture, p.87-97, December 2000, Monterey, California, United States [doi>10.1145/360128.360139]
• 9: D. Cyrluk, "Microprocessor Verification in PVS: A Methodology and Simple Example," Technical Report SRI-CSL-93-12, SRI Computer Science Laboratory, 1993.
• 10: Anuj Goel , Khurram Sajid , Hai Zhou , Adnan Aziz , Vigyan Singhal, BDD Based Procedures for a Theory of Equality with Uninterpreted Functions, Proceedings of the 10th International Conference on Computer Aided Verification, p.244-255, June 28-July 02, 1998
• 11: W. A. Hunt, "FM8501: A Verified Microprocessor," Tech. Rept. 47, Institute for Computing Science, University of Texas at Austin, 1986.
• 12: J. Joyce, "Formal Verification and Implementation of a Microprocessor, "VLSI Specification, Verification, and Synthesis, G. Birtwistle and P. A. Subrahmanyam, eds., Kulwer Academic Publishers, 1988.
• 13: Kanna Shimizu , David L. Dill , Alan J. Hu, Monitor-Based Formal Specification of PCI, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.335-353, November 01-03, 2000
• 14: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 15: 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]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Microprocessor/microcomputer applications

Additional Classification:
  C. Computer Systems Organization

  J. Computer Applications
  J.2 PHYSICAL SCIENCES AND ENGINEERING
      Subjects: Electronics

General Terms:
Design, Experimentation, Measurement, Performance, Theory, Verification