FM8501: A Verified Microprocessor

Front Cover
Springer Science & Business Media, May 20, 1994 - Computers - 333 pages
The 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
Index
316
References
330
Copyright

Other editions - View all

Common terms and phrases