Formal Verification of Explicitly Parallel Microprocessors

  • Byron Cook
  • John Launchbury
  • John Matthews
  • Dick Kieburtz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


The trend in microprocessor design is to extend instruction-set architectures with features—such as parallelism annotations, predication, speculative memory access,or multimedia instructions—that allow the compiler or programmer to express more instruction-level parallelism than the microarchitecture is willing to derive. In this paper we show how these instruction-set extensions can be put to use when formally verifying the correctness of a microarchitectural model. Inspired by Intel’s IA-64, we develop an explicitly parallel instruction-set architecture and a clustered microarchitectural model. We then describe how to formally verify that the model implements the instruction set. The contribution of this paper is a specification and verification method that facilitates the decomposition of microarchitectural correctness proofs using instruction-set extensions.


State Machine Program Counter Java Virtual Machine Uninterpreted Function Completion Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Martin Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 2(82):253–284, 1991.CrossRefMathSciNetGoogle Scholar
  2. 2.
    J.R. Allen, K. Kennedy, C. Porterfield, and J. Warren. Conversion of control dependence to data dependence. In The 10th ACM Symposium on Principles of Programming Languages, January 1983.Google Scholar
  3. 3.
    David Bistry, Carole Delong, Mickey Gutman, Michael Julier, Michael Keith, Lawrence M. Mennemeir, Millind Mittal, Alex D. Peleg, and Uri Weiser. The Complete Guide to MMX Technology. McGraw-Hill, 1997.Google Scholar
  4. 4.
    Jerry Burch and David Dill. Automatic verification of pipelined microprocessor control. In 6th International Conference of Computer Aided Verification, Stanford, California, June 1994.Google Scholar
  5. 5.
    Brian Case. IA-64’s static approach is controversial. Microprocessor Report, 11(16), 1997.Google Scholar
  6. 6.
    Werner Damm and Amir Pnueli. Verifying out-of-order executions.In Conference on Correct Hardware Design and Verification Methods,Montreal,Canada, 1997.Google Scholar
  7. 7.
    Keith Deifendorff. WinChip 4 thumbs nose at ILP. Microprocessor Report, 12(16), 1998.Google Scholar
  8. 8.
    Carole Delong. The IA-64 architecture at work. IEEE Computer, 31(7), 1998.Google Scholar
  9. 9.
    Kieth Diefendorff. Microarchitecture in the ditch. Microprocessor Report, 12(17), 1998.Google Scholar
  10. 10.
    Linley Gwennap. Intel’s P6 uses decoupled superscalar design. Microprocessor Report, 9(2), 1995.Google Scholar
  11. 11.
    Linley Gwennap. Digital 21264 sets new standard. itMicroprocessor Report, 14(10), 1996.Google Scholar
  12. 12.
    Linley Gwennap. Intel, HP make EPIC disclosure. Microprocessor Report, 11(14), 1997.Google Scholar
  13. 13.
    Linley Gwennap. AltiVec vectorizes PowerPC. Microprocessor Report, 12(6), 1998.Google Scholar
  14. 14.
    Linley Gwennap. AMD deploys K6-2 with 3DNow. Microprocessor Report, 12 (7), 1998.Google Scholar
  15. 15.
    Linley Gwennap. Intel outlines high-end roadmap. Microprocessor Report, 12(14), 1998.Google Scholar
  16. 16.
    John L. Hennessy and David A. Patterson. Computer Architecture:A Quantitative Approach. Morgan Kaufmann, 1995.Google Scholar
  17. 17.
    Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran. An assume-guarantee rule for checking simulation. In Formal Methods in Computer-Aided Design, Palo Alto, California, 1998.Google Scholar
  18. 18.
    Richard C. Ho, C. Han Yang, Mark A. Horowitz, and David Dill. Architecture validation for processors. In Proceedings of the 22nd Annual International Symposium on Computer Architecture, Santa Margherita Ligure, Italy, 1995.Google Scholar
  19. 19.
    Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan. Decomposing the proof of correctness of pipelined microprocessors. In International Conference on Computer-Aided Verification, Vancouver, Canada, July 1998.Google Scholar
  20. 20.
    Dave Jaggar. Advanced RISC Machines Architectural Reference Manual. Prentice Hall, 1997.Google Scholar
  21. 21.
    David Johnson. Techniques for mitigating memory latency in the the PA-8500 processor. In Hot Chips 10, Palo Alto, August 1998.Google Scholar
  22. 22.
    Mike Johnson. Superscalar Microprocessor Design. Prentice Hall, 1991.Google Scholar
  23. 23.
    Robert B. Jones, David L. Dill, and Jerry R. Burch. Efficient validity checking for processor verification. In Proceedings of the 1995 International Conference on Computer-Aided Design, San Jose, 1995.Google Scholar
  24. 24.
    Vinod Kathail, Michael Schlansker, and B. Ramakrishna Rau. HPL PlayDoh architecture specification: Version 1.0. Technical Report HPL-93-80, Hewlett Packard Laboratories, 1993.Google Scholar
  25. 25.
    Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison Wesley, 1997.Google Scholar
  26. 26.
    Ken McMillan. Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In International Conference on Computer-Aided Verification, Vancouver, Canada, July 1998.Google Scholar
  27. 27.
    R. Milner. An algebraic definition of simulation between programs. In Proceedings of 2nd International Joint Conference on Artificial Intelligence, The British Computer Society, 1971.Google Scholar
  28. 28.
    Zhenyu Qian. A formal specification of a large subset of Java virtual machine instructions for objects, methods and subroutines. In Formal Syntax and Semantics of Java. Springer-Verlog, 1998.Google Scholar
  29. 29.
    B. Ramakrishna Rau and Joseph A. Fisher. Instruction-level parallel processing: History, overview and perspective. The Journal of Supercomputing, 7(1), 1993.Google Scholar
  30. 30.
    Jun Sawada and Warren Hunt. Processor verification with precise exceptions and speculative execution.In International Conference on Computer-Aided Verification, Vancouver,Canada,July 1998.Google Scholar
  31. 31.
    Michael Schlansker, B.Ramakrishna Rau,, Scott Mahlke, Vinod Kathail, Richard Johnson, Sdum Anik,and Santosh G. Abraham. Achieving high levels of instruction-level parallelism with reduced hardware complexity.Technical Report HPL-96-120,Hewlett Packard Laboratories, 1996.Google Scholar
  32. 32.
    Bruce Shriver and Bennett Smith. The Anatomy of a High-Performance Microprocessor: A Systems Perspective. IEEE Computer Society Press, 1998.Google Scholar
  33. 33.
    Jens Skakkebaek, Robert Jones, and David Dill. Formal verification of out-of-order execution using incremental flushing. In International Conference on Computer-Aided Verification, Vancouver, Canada, July 1998.Google Scholar
  34. 34.
    Peter Song. Demystifying EPIC and IA-64. Microprocessor Report, 12(1), 1998.Google Scholar
  35. 35.
    E.W. Stark. Ap roof technique for rely/guarantee properties. In Proceedings of the 5th Conference on Foundations of Software Technology and Theoretical Computer Science, August 1985.Google Scholar
  36. 36.
    Karen Stephenson. Towards an algebraic specification of the Java virtual machine. In Prospects for Hardware Foundations. Springer-Verlog, 1998.Google Scholar
  37. 37.
    Dean M. Tullsen, Susan J. Eggers, Joel S. Emer, Henry M. Levy, Jack L. Lo, and Rebecca L. Stamm. Exploiting choice: Instruction fetch and issue on an implementable simultaneous multithreading processor. In 23rd Annual International Symposium on Computer Architecture, Philadelphia, PA, May 1996.Google Scholar
  38. 38.
    Miroslav N. Velev and Randal E. Bryant. Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking. In FormalMethods in Computer-Aided Design, Palo Alto, California, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Byron Cook
    • 1
  • John Launchbury
    • 1
  • John Matthews
    • 1
  • Dick Kieburtz
    • 1
  1. 1.Oregon Graduate InstituteUSA

Personalised recommendations