Technical reports
Hardware verification using higher-order logic
Albert Camilleri, Mike Gordon, Tom Melham
September 1986, 25 pages
DOI: 10.48456/tr-91
Abstract
The Hardware Verification Group at the University of Cambridge is investigating how various kinds of digital systems can be verified by mechanised formal proof. This paper explains our approach to representing behaviour and structure using higher order logic. Several examples are described including a ripple carry adder and a sequential device for computing the factorial function. The dangers of inaccurate models are illustrated with a CMOS exclusive-or gate.
Full text
PDF (1.3 MB)
BibTeX record
@TechReport{UCAM-CL-TR-91, author = {Camilleri, Albert and Gordon, Mike and Melham, Tom}, title = {{Hardware verification using higher-order logic}}, year = 1986, month = sep, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-91.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-91}, number = {UCAM-CL-TR-91} }