Abstract
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.
Acknowledgments
Mark Aagaard, Todd Austin,Nancy Day,Sava Krstić, Bee Lavender,Tim Leonard,Abdelillah Mokkedem, John O’Leary, Mark Shields, and the anonymous reviewers:thank you for your comments,suggestions and support.
Funding for this research was provided by Intel Corporation,the U.S.National Security Agency,and the U.S.Air Force Material Command (F19628-93- C-0069). John Matthews is supported by a fellowship from the U.S.National Science Foundation.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Martin Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 2(82):253–284, 1991.
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.
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.
Jerry Burch and David Dill. Automatic verification of pipelined microprocessor control. In 6th International Conference of Computer Aided Verification, Stanford, California, June 1994.
Brian Case. IA-64’s static approach is controversial. Microprocessor Report, 11(16), 1997.
Werner Damm and Amir Pnueli. Verifying out-of-order executions.In Conference on Correct Hardware Design and Verification Methods,Montreal,Canada, 1997.
Keith Deifendorff. WinChip 4 thumbs nose at ILP. Microprocessor Report, 12(16), 1998.
Carole Delong. The IA-64 architecture at work. IEEE Computer, 31(7), 1998.
Kieth Diefendorff. Microarchitecture in the ditch. Microprocessor Report, 12(17), 1998.
Linley Gwennap. Intel’s P6 uses decoupled superscalar design. Microprocessor Report, 9(2), 1995.
Linley Gwennap. Digital 21264 sets new standard. itMicroprocessor Report, 14(10), 1996.
Linley Gwennap. Intel, HP make EPIC disclosure. Microprocessor Report, 11(14), 1997.
Linley Gwennap. AltiVec vectorizes PowerPC. Microprocessor Report, 12(6), 1998.
Linley Gwennap. AMD deploys K6-2 with 3DNow. Microprocessor Report, 12 (7), 1998.
Linley Gwennap. Intel outlines high-end roadmap. Microprocessor Report, 12(14), 1998.
John L. Hennessy and David A. Patterson. Computer Architecture:A Quantitative Approach. Morgan Kaufmann, 1995.
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.
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.
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.
Dave Jaggar. Advanced RISC Machines Architectural Reference Manual. Prentice Hall, 1997.
David Johnson. Techniques for mitigating memory latency in the the PA-8500 processor. In Hot Chips 10, Palo Alto, August 1998.
Mike Johnson. Superscalar Microprocessor Design. Prentice Hall, 1991.
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.
Vinod Kathail, Michael Schlansker, and B. Ramakrishna Rau. HPL PlayDoh architecture specification: Version 1.0. Technical Report HPL-93-80, Hewlett Packard Laboratories, 1993.
Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison Wesley, 1997.
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.
R. Milner. An algebraic definition of simulation between programs. In Proceedings of 2nd International Joint Conference on Artificial Intelligence, The British Computer Society, 1971.
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.
B. Ramakrishna Rau and Joseph A. Fisher. Instruction-level parallel processing: History, overview and perspective. The Journal of Supercomputing, 7(1), 1993.
Jun Sawada and Warren Hunt. Processor verification with precise exceptions and speculative execution.In International Conference on Computer-Aided Verification, Vancouver,Canada,July 1998.
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.
Bruce Shriver and Bennett Smith. The Anatomy of a High-Performance Microprocessor: A Systems Perspective. IEEE Computer Society Press, 1998.
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.
Peter Song. Demystifying EPIC and IA-64. Microprocessor Report, 12(1), 1998.
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.
Karen Stephenson. Towards an algebraic specification of the Java virtual machine. In Prospects for Hardware Foundations. Springer-Verlog, 1998.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cook, B., Launchbury, J., Matthews, J., Kieburtz, D. (1999). Formal Verification of Explicitly Parallel Microprocessors. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_4
Download citation
DOI: https://doi.org/10.1007/3-540-48153-2_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66559-5
Online ISBN: 978-3-540-48153-9
eBook Packages: Springer Book Archive