Computer Laboratory

Technical reports

Simulation as an aid to verification using the HOL theorem prover

Albert John Camilleri

October 1988, 23 pages

Abstract

The HOL theorem proving system, developed by Mike Gordon at the University of Cambridge, is a mechanism of higher order logic, primarily intended for conducting formal proofs of digital system designs. In this paper we show that hardware specifications written in HOL logic can be executed to enable simulation as a means of supporting formal proof. Specifications of a small microprocessor are described, showing how HOL logic sentences can be transformed into executable code with minimum risk of introducing inconsistencies. A clean and effective optimisation strategy is recommended to make the executable specifications practical.

Full text

PDF (1.7 MB)

BibTeX record

@TechReport{UCAM-CL-TR-150,
  author =	 {Camilleri, Albert John},
  title = 	 {{Simulation as an aid to verification using the HOL theorem
         	   prover}},
  year = 	 1988,
  month = 	 oct,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-150.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-150}
}