The FM8501 Microprocessor

Warren Hunt's Ph. D. dissertation is now available as the book ``FM8501: A Verified Microprocessor,'' LNCS 795. Springer-Verlag. 1994. The actual Nqthm events for the specification and verification is part of the Nqthm-1992 ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/README.html.

Abstract

Digital computer hardware can be described and specified mathematically. Formal representation of computing devices has many advantages: automated verification, symbolic execution, and symbolic reasoning. Formal specification of digital computing devices yields unambiguous meaning for hardware functions. This work demonstrates the use of formal logic as a representation format for a digital logic. Associated with this formal logic is an automated reasoning system that allows mechanical verification to be performed. Hardware devices are described by recursive functions. Through verification, it can be shown that hardware devices actually possess desired mathematical properties. Once these hardware devices are defined it is possible to execute them, thus providing a simulation capability for digital hardware devices. If the sizes of the data paths, words, etc., are fixed, the recursive functions can be expanded into Boolean logic and registers. The primary result of this research is the formal definition and specification of a microprocessor; along with the proofs that the formal definition satisfies the specifications. This microprocessor, which has a user-mode instruction set inspired by the PDP-11, has been verified for three mathematically constructed data-types: Boolean vectors, natural numbers, and integers.