Technical reports
Why higher-order logic is a good formalisation for specifying and verifying hardware
September 1985, 28 pages
DOI: 10.48456/tr-77
Abstract
Higher order logic was originally developed as a foundation for mathematics. In this paper we show how it can be used as: 1. a hardware description language, and 2. a formalism for proving that designs meet their specifications.
Examples are given which illustrate various specification and verification techniques. These include a CMOS inverter, a CMOS full adder, an n-bit ripple-carry adder, a sequential multiplier and an edge-triggered D-type register.
Full text
PDF (0.9 MB)
BibTeX record
@TechReport{UCAM-CL-TR-77, author = {Gordon, Mike}, title = {{Why higher-order logic is a good formalisation for specifying and verifying hardware}}, year = 1985, month = sep, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-77.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-77}, number = {UCAM-CL-TR-77} }