Department of Computer Science and Technology

Technical reports

Hardware verification by formal proof

Mike Gordon

August 1985, 6 pages

DOIhttps://doi.org/10.48456/tr-74

Abstract

The use of mathematical proof to verify hardware designs is explained and motivated. The hierarchical verification of a simple n-bit CMOS counter is used as an example. Some speculations are made about when and how formal proof will become used in industry.

Full text

PDF (0.4 MB)

BibTeX record

@TechReport{UCAM-CL-TR-74,
  author =	 {Gordon, Mike},
  title = 	 {{Hardware verification by formal proof}},
  year = 	 1985,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-74.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-74},
  number = 	 {UCAM-CL-TR-74}
}