Formal Verification and Implementation of a Microprocessor

Mike Gordon has described the specification and verification of a microcoded computer using the LCF_LSM hardware verification system [8]. We have subsequently redone this example in higher-order logic using the HOL system [10]. In this paper we present the specification of Gordon’s computer in higherorder logic and a brief explanation of its formal verification. A more detailed discussion of the formal verification may be found in [16]. We also describe several related examples of hardware verification based on Gordon’s computer and other microprocessor designs. Finally, we report experience in using a formal specification to implement Gordon’s computer as a 5,000 transistor CMOS microchip.