PRISM (University of Calgary) · 1985 · 38 citations · 0 references
ComputingComputer ScienceMathematicsFormal MethodsLogicTheory Of ComputationAutomated ReasoningDeductive VerificationMathematical LogicModel CheckingPredicate LogicTheorem ProvingHigher-order Logic
Mike Gordon has described the specification and verification of a register-transfer level implementation of a simple general purpose computer using the LCF_LSM hardware verification system [1] [2]. We have subsequently redone this example in higher order logic using the HOL system [3]. In this paper we present the specification and verification of Gordon's computer as an example of hardware specification and verification in higher order logic.