Technical reports

Proving a computer correct in higher order logic

Jeff Joyce, Graham Birtwistle, Mike Gordon

December 1986, 57 pages

DOI: 10.48456/tr-100

Abstract

Technical report no. 42, ‘Proving a computer correct using the LSF_LSM hardware verification system’, describes the specification and verification of a register-transfer level implementation of a simple general purpose computer. The computer has a microcoded control unit implementing eight user level instructions. We have subsequently redone this example in higher order logic using the HOL hardware verification system.

This report presents the specification and verification of Gordon’s computer as an example of hardware specification and verification in higher order logic. The report describes how the structure and behaviour of digital circuits may be specified using the formalism of higher order logic. The proof of correctness also shows how digital behaviour at different granularities of time may be related by means of a temporal abstraction.

This report should be read with Technical report no. 68, ‘HOL, a machine oriented formulation of higher order logic’, which describes the logic underlying the HOL hardware verification system.

Full text

Only available on paper (could be scanned on request).

BibTeX record

@TechReport{UCAM-CL-TR-100,
  author =	 {Joyce, Jeff and Birtwistle, Graham and Gordon, Mike},
  title = 	 {{Proving a computer correct in higher order logic}},
  year = 	 1986,
  month = 	 dec,
  institution =  {University of Cambridge, Computer Laboratory},
  address =	 {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom,
          	  phone +44 1223 763500},
  doi = 	 {10.48456/tr-100},
  number = 	 {UCAM-CL-TR-100}
}