Joyce, JeffreyBirtwistle, Graham2008-02-272008-02-271985-08-01http://hdl.handle.net/1880/45721Mike 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.EngComputer Scienceunknown1985-208-2110.11575/PRISM/30386