Verifying correct pipeline implementation for microprocessors

ABSTRACT

We introduce a general, automatic verification technique for pipelined designs. The technique is based on a scalable, formal methodology for analyzing pipelines. The key advantages to our technique are: it specifically targets pipeline control, making it more efficient; it requires no explicit specification, since it compares hardware against itself; it can be used within the broader framework of hierarchical verification; and, it can be easily extended to handle certain "complex" pipelined structures.

REFERENCES

• 1: 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]
• 2: 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
• 3: 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
• 4: 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 [doi>10.1145/240518.240623]
• 5: 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 [doi>10.1145/240518.240624]
• 6: John L. Hennessy , David A. Patterson, Computer architecture (2nd ed.): a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 7: 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
• 8: M. C. McFarland, "Formal Verification of Sequential Hardware: A Tutorial," IEEE Transactions on computer- Aided Design of lntegrated Circuits and Systems, vol. 12, no. 5, May 1993.
• 9: K. L. McMillan, Fitting formal methods into the design cycle, Proceedings of the 31st annual conference on Design automation, p.314-319, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196392]
• 10: 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.1 PROCESSOR ARCHITECTURES
      C.1.2 Multiple Data Stream Architectures (Multiprocessors)
          Subjects: Pipeline processors**

Additional Classification:
  C. Computer Systems Organization

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