Department of Computer Science and Technology

Technical reports

Why higher-order logic is a good formalisation for specifying and verifying hardware

Mike Gordon

September 1985, 28 pages

DOIhttps://doi.org/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}
}