Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

During the recent development of a next-generation Intel processor, the project's formal verification team verified a new coherence protocol and portions of its RTL implementation against the protocol's specification within project deadlines. Typically, FV teams apply formal property verification (FPV) after RTL is coded and, though it continues to be an effective complement to pre-silicon validation, this late application prevents it from keeping pace with the continual complexity increases in hardware designs. Our discussion centers around how applying FV early in the development cycle of this processor enabled continual verification as the design progressed, culminating with the targeted RTL verification. We also present the languages and methodologies used, the reasons behind the choices, and where improvements can be made.

REFERENCES

• 1: Mani Azimi , Ching-Tsun Chou , Akhilesh Kumar , Victor W. Lee , Phamndra K. Mannava , Seungjoon Park, Experience with Applying Formal Methods to Protocol Specification and System Architecture, Formal Methods in System Design, v.22 n.2, p.109-116, March 2003 [doi>10.1023/A:1022965204416]
• 2: B. Batson and L. Lamport. High-level specifications: Lessons from industry. In Formal Methods for Components and Objects, volume 2852/2003 of Lecture Notes in Computer Science, pages 242--261, 2003.
• 3: Bob Bentley, Validating the intel pentium 4 microprocessor, Proceedings of the 38th conference on Design automation, p.244-248, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378473]
• 4: 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
• 5: A. Camilleri, M. Gordon, and T. Melham. Hardware Verification Using Higher-Order Logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 43--67. North-Holland, 1986.
• 6: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, Carnegie Mellon University, Pittsburgh, PA, 1987
• 7: G. Gopalakrishnan, E. Brunvand, N. Michell, and S. M. Nowick. A Correctness Criterion for Asynchronous Circuit Validation and Optimization. IEEE Trans. on Computer Aided Design, 13(11):1309--1318, November 1994.
• 8: John Harrison, Formal Verification of Square Root Algorithms, Formal Methods in System Design, v.22 n.2, p.143-153, March 2003 [doi>10.1023/A:1022973506233]
• 9: Roope Kaivola , Mark Aagaard, Divider Circuit Verification with Model Checking and Theorem Proving, Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, p.338-355, August 14-18, 2000
• 10: R. Kaivola , N. Narasimhan, Formal Verification of the Pentium® 4 Floating-Point Multiplier, Proceedings of the conference on Design, automation and test in Europe, p.20, March 04-08, 2002
• 11: Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 12: T. F. Melham. Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic. PhD thesis, University of Cambridge, 1990.
• 13: Tom Schubert, High level formal verification of next-generation microprocessors, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775834]
• 14: Yuan Yu , Panagiotis Manolios , Leslie Lamport, Model Checking TLA+ Specifications, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.54-66, September 27-29, 1999

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Algorithms, Design, Verification

Keywords:
TLA+, TLC, explicit state enumeration, formal verification, microarchitecture verification, protocol verification