FM8501: A Verified MicroprocessorThe FM 8501 microprocessor was invented as a generic microprocessor somewhat similar to a PDP-11. The principal idea of the FM 8501 effort was to see if it was possible to express the user-level specification and the design implementation using a formal logic, the Boyer-Moore logic; this approach permitted a complete mechanically checked proof that the FM 8501 implementation fully implemented its specification. The implementation model for the FM 8501 was inadequate for industrial hardware design but the effort was an important step in the evolution to the design verification methodology now employed by the author. The original version of this monograph was submitted as a dissertation at the University of Texas at Austin under the advisorship of R. Boyer and J. Moore. |
What people are saying - Write a review
We haven't found any reviews in the usual places.
Contents
Introduction | 1 |
12 The Meaning of Verification | 2 |
14 Dissertation Outline | 4 |
A Hardware Model | 5 |
22 The Registertransfer Model | 6 |
23 The FM8501 Model | 8 |
24 Related Hardware Verification Efforts | 9 |
Notation and Bit Vectors | 13 |
The ALU | 55 |
81 ALU Hardware Function | 56 |
82 ALU Specification | 58 |
Instruction Fields | 69 |
Update and Accessor Functions | 73 |
The FM8501 Hardware Interpreter | 75 |
111 The Control Unit | 78 |
112 Miscellanous Functions | 81 |
32 The BoyerMoore Logic | 14 |
33 Bit Vectors | 16 |
Numeric Definitions and Operations | 19 |
41 Natural Number Representation | 20 |
412 Bitvectors for Natural Numbers | 21 |
42 Integer Number Representation | 23 |
422 Bitvectors for Integer Numbers | 24 |
The Verification Approach | 27 |
FM8501 A Conventional Description | 31 |
62 Block Diagram | 32 |
64 Data Representation | 34 |
66 Addressing | 35 |
68 Signal Description | 36 |
684 Reset Input | 38 |
69 Bus Operation | 39 |
Commonly Used Functions | 41 |
72 Adder and Subtracter Definitions | 51 |
73 Incrementer and Decrementer | 53 |
113 The FM8501 Combinational Logic | 83 |
114 External Functions | 89 |
FM8501 A Formal Specification | 93 |
123 Conditional Storage of the ALU Results | 94 |
124 Register File Update | 95 |
125 Memory Update | 100 |
127 The Reset Specification | 101 |
Correctness of FM8501 | 103 |
132 Resetting FM8501 | 104 |
133 Abstracting BigMachines State | 106 |
134 The Oracles | 107 |
135 Correctness of FM8501 Instruction Execution | 109 |
Expansion of FM8501 | 111 |
Conclusions | 143 |
FM8501 Formulas | 146 |
| 316 | |
References | 330 |
Other editions - View all
Common terms and phrases
19 b-nand b-nand a-reg b-reg c-flag a-reg b-reg i-reg a-reg-after-a-b add bv-to-tc addr-out c-flag v-flag b-nand 18 b-xor b-nand 22 b-nand b-nand b-nand 18 b-not b-or b-and b-reg i-reg visual-mem b-xor bit-vector bitn i-reg bitv b-nand b-nand bitvp boolp bv bv-alu-cv bv-alu-cv a b c nat-to-bv bv-cv bv-oprd-b bv-to-nat c a b c-flag v-flag z-flag carry current-instruction reg-file real-mem data-out addr-out data-out reg-file addr-out defined definition defn difference disable dtack enable equal a btm formal function hardware i-reg visual-mem real-mem implies input instruction lessp list f f machine-size memory micro-rom mar move n-flag a-reg b-reg natural number negativep no-store data-out reg-file nth 0 reg-file nxsz operation oracle prove-lemma real-mem watch-dog reg-file addr-out c-flag reg-file real-mem c-flag remainder reset returns rewrite sizep specification sub1 tc-minus update-nth v-flag z-flag n-flag v-nat-dec v-nat-inc v-nth z-flag n-flag a-reg zerop