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
distribution.
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.
http://dirleton.csres.utexas.edu/hardware/fm8501.html
This page is URL http://www.computationallogic.com/hardware/fm8501.html