Computer Laboratory

Technical reports

Hardware verification using higher-order logic

Albert Camilleri, Mike Gordon, Tom Melham

September 1986, 25 pages

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 = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-91.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-91}
}