Technical reports
Simulation as an aid to verification using the HOL theorem prover
Albert John Camilleri
October 1988, 23 pages
DOI: 10.48456/tr-150
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 = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-150.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-150}, number = {UCAM-CL-TR-150} }