Formal Verification of the
Paliath Narendran, Jonathan Stillman · 1988
We describe an approach to hardware verification in the context of our recent success in formally verifying the description of an image processing chip currently under development at Research Triangle Institute. We demonstrste that our approach, which uses an implementation of an equational approach to theorem proving developed by Kapur and Narendran, can be a viable alternative to simulation. In particular, we are able to take advantage of the “recursive” nature of many circuits, such as n-bit adders, and our techniques allow verification of sequential circuits. To the best of our knowledge this is the first time a complex sequential circuit which was not designed with formal verification specifically in mind has been verified. Finally, we describe the discovery of several design errors in the circuit description, detected during the verification attempt (the actual verification could only take place once these errors were removed), and discuss directions that future work will take. A significantly more detailed description of this work can be found in [NaSt 881.