Department of Computer Science and Technology

Technical reports

A formal hardware verification methodology and its application to a network interface chip

M.J.C. Gordon, J. Herbert

May 1985, 39 pages

Abstract

We describe how the functional correctness of a circuit design can be verified by machine checked formal proof. The proof system used is LCF_LSM [1], a version of Milner’s LCF [2] with a different logical calculus called LSM. We give a tutorial introduction to LSM in the paper.

Our main example is the ECL chip of the Cambridge Fast Ring (CFR) [3]. Although the ECL chip is quite simple (about 360 gates) it is nevertheless real. Minor errors were discovered as we performed the formal proof, but when the corrected design was eventually fabricated it was functionally correct first time. The main steps in verification were: (1) Writing a high-level behavioural specification in the LSM notation. (2) Translating the circuit design from its Modula-2 representation in the Cambridge Design Automation System [4] to LSM. (3) Using the LCF_LSM theorem proving system to mechanically generate a proof that the behaviour determined by the design is equivalent to the specified behaviour.

In order to accomplish the second of these steps, an interface between the Cambridge Design Automation System and the LCF_LSM system was constructed.

Full text

PDF (1.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-66,
  author =	 {Gordon, M.J.C. and Herbert, J.},
  title = 	 {{A formal hardware verification methodology and its
         	   application to a network interface chip}},
  year = 	 1985,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-66.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-66}
}