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

From bibtex.

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 the verification were: Writing a high-level behavioural specification in the LSM notation. Translating the circuit design from its Modula-2 representation in the Cambridge Design Automation System [4] to LSM. 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.