|
|
|---|
|
|
|
|---|
W. A. Hunt, Jr., FM8501: A Verified Microprocessor,
University of Texas at Austin, Ph.D. dissertation, 1985 (also published as a
book of the same title, Springer-Verlag LNAI 795, Heidelberg, 1994.
Relevance: first microprocessor verified at the gate
level and the bottommost component of the CLI stack
The precursor to the verified microprocessor used in the CLI Verified
Stack as reported in bib::bhmy89 is described here. See the Nqthm
script
FM8501, which had 8 registers and a 16-bit wordsize, was verified to implement a conventional orthogonal instruction set. The semantics of the gate-level design of the FM8501 and of the instruction set were described operationally. The CLI Stack was ultimately based on the FM8502, which was like the FM8501 except (a) the wordsize was 32-bits and (b) extra bits were allocated in the instruction word to permit programmer control over ALU condition code flags. These changes were requested by Moore during his design of an assembler for the machine. For more detail on the evolutionary pressure that the assembler put on the underlying machine see Section 1.5 of bib::moore96. Since the gate-level design of the FM8501 was parameterized by the word length (including the ALU), the description and verification of the 32-bit FM8502 was easier for Hunt than one might otherwise expect. The FM8502 is described in more detail in Hunt's article in bib::bhmy89. Because of the way the gate-level designs of FM8501 and FM8502 were expressed, it was impractical to fabricate either machine. However, see bib::hb92.