|
|
|---|
|
|
|
|---|
W. A. Hunt, Jr. and B. Brock, “A
Formal HDL and its use in the FM9001 Verification”, Proceedings
of the Royal Society, North Holland, April, 1992.
Relevance: a formalized hardware description language
and the verification of a fabricated microprocessor described with it; this
describes three foundational achievements in formal methods
Abstract
A synchronous, hierarchical, occurrence-oriented, hardware description language (HDL) has been formalized with the Boyer-Moore logic. Well-formed HDL circuits are recognized by a predicate, and a unit-clock simulator defines the meaning of circuits expressed in the HDL. This HDL has been used to specify an implementation of the FM9001 microprocessor that has been mechanically proved to implement the FM9001 instruction-level specification. All proofs were mechanically checked using the Boyer-Moore theorem-proving system. The formalization of the HDL, the FM9001 user-level specification, and the FM9001 HDL implementation architecture specification required more than 700 function definitions. The mechanical proof is composed of thousands of theorem prover proof requests and millions of theorem prover inference steps.
The verified fabricated microprocessor described here was used in the final hosting of the CLI Verified Stack bib::bhmy89.
But aside from its importance to the Verified Stack, this paper describes three foundational achievements in formal methods:
For complete details, see the Nqthm script