Abstract
This paper presents techniques for specifying microprocessor instruction set syntax and semantics in the HOL theorem proving system. The paper describes the use of abstract representations for operators and data, gives techniques for specifying instruction set syntax, outlines the use of records in specifying semantic domains, presents the creation of parameterized semantic frameworks, and shows how all of these can be used to create a semantics for a microprocessor instruction set. The verified microprocessor Uinta provides examples for each of these.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Jonathan P. Bowen. Formal specification and documentation of microprocessor instruction sets. In Microprocessing and Microprogramming 21, pages 223–230, 1987.
S. D. Crocker, E. Cohen, S. Landauer, and H. Orman. Reverification of a microprocessor. In Proceedings of the IEEE Symposium on Security and Privacy, pages 166–176, April 1988.
Avra Cohn. Correctness properties of the VIPER block model: The second level. Technical Report 134, University of Cambridge Computer Laboratory, May 1988.
Avra Cohn. A proof of correctness of the VIPER microprocessor: The first level. In G. Birtwhistle and P. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis, pages 27–72. Kluwer Academic Publishers, 1988.
Michael J.C. Gordon. Proving a computer correct. Technical Report 41, Computer Lab, University of Cambridge, 1983.
Jody W. Gambles and Phillip J. Windley. Integrating formal verification with CAD tool environments. Technical Report LAL-92-02, University of Idaho, Laboratory for Applied Logic, April 1992. In review, Formal Methods in System Design.
John Herbert. Incremental design and formal verification of microcoded microprocessors. In V. Stavridou, T. F. Melham, and R. T. Boute, editors, Theorem Provers in Circuit Design, Proceedings of the IFIP WG 10.2 International Working Conference, Nijmegen, The Netherlands. North-Holland, June 1992.
Warren A. Hunt. The mechanical verification of a microprocessor design. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. Elsevier Scientific Publishers, 1987.
Warren A. Hunt. Microprocessor design verification. Journal of Automated Reasoning, 5:429–460, 1989.
Jeffrey J. Joyce. Formal verification and implementation of a microprocessor. In G. Birtwhistle and P.A Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis. Kluwer Academic Press, 1988.
Jeffrey J. Joyce. Multi-Level Verification of Microprocessor-Based Systems. PhD thesis, Cambridge University, December 1989.
Timothy E. Leonard. Specification of computer architectures. Technical report, Cambridge University Computer Laboratory, 1989.
M. Srivas and M. Bickford. Formal verification of a pipelined microprocessor. IEEE Software, 7(5):52–64, September 1990.
E. Thomas Schubert, Phillip J. Windley, and Karl Levitt. Report on the ucd microcoded viper verification project. In Jeffery J. Joyce and Carl Seger, editors, Proceedings of the 1993 International Workshop on the HOL Theorem Prover and its Applications., August 1993.
Sofiene Tahar and Ramayya Kumar. Implementing a methodology for formally verifying RISC processors in HOL. In Jeffery J. Joyce and Carl Seger, editors, Proceedings of the 1993 International Workshop on the HOL Theorem Prover and its Applications., August 1993.
Phillip J. Windley and Michael Coe. The formal verification of instruction pipelines. Technical Report LAL-94-01, Brigham Young University, Laboratory for Applied Logic, February 1994. (submitted to Theorem Provers in Circuit Design 94).
Glynn Winskel. Models and logic in MOS circuits. In M. Broy, editor, Logic of Programming and Calculi of Discrete Designs: International Summer School Directed by F. L. Bauer, M. Broy, E. W. Dijkstra, and C. A. R. Hoare, volume 36 of NATO ASI Series, Series F: Computer and Systems Sciences, pages 367–413. Springer-Verlag, 1987.
Phillip J. Windley. The Formal Verification of Generic Interpreters. PhD thesis, University of California, Davis, Division of Computer Science, June 1990.
Phillip J. Windley. A hierarchical methodology for the verification of microprogrammed microprocessors. In Proceedings of the IEEE Symposium on Security and Privacy, May 1990.
Phillip J. Windley. Abstract theories in HOL. In Luc Claesen and Michael J. C. Gordon, editors, Proceedings of the 1992 International Workshop on the HOL Theorem Prover and its Applications. North-Holland, November 1992.
Phillip J. Windley. Documentation for the records library. Technical Report LAL-93-15, Brigham Young University, Laboratory for Applied Logic, July 1993. (Available electronically at URL: http://lal.cs.byu.edu/lal/ holdoc/library/records/records.html).
Phillip J. Windley. A theory of generic interpreters. In George J. Milne and Laurence Pierre, editors, Correct Hardware Design and Verification Methods, number 683 in Lecture Notes in Computer Science, pages 122–134. Springer-Verlag, 1993.
Phillip J. Windley. Formal modeling and verification of microprocessors. IEEE Transactions on Computers, 1994. (to appear).
Wai Wong and Tom Melham. The HOL wordn library. In HOL System Library Documentation. University of Cambridge Computer Laboratry, October 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Windley, P.J. (1994). Specifying instruction-set architectures in HOL: A primer. In: Melham, T.F., Camilleri, J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58450-1_59
Download citation
DOI: https://doi.org/10.1007/3-540-58450-1_59
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58450-6
Online ISBN: 978-3-540-48803-3
eBook Packages: Springer Book Archive