Design Automation Conference (1988)
Anaheim, CA, USA
June 12, 1988 to June 15, 1988
Narendran , Gen. Electr. Co., Schenectady, NY, USA
An approach is described for hardware verification in the context of the authors' recent success in formally verifying the description of an image-processing chip. They demonstrate that their approach, which uses an implementation of an equational approach to theorem proving developed by D. Kapur and P. Narendran (1985), can be a viable alternative to simulation. In particular, they are able to take advantage of the recursive nature of many circuits, such as n-bit adders, and their techniques allow verification of sequential circuits. To the best of their knowledge this is the first time a complex sequential circuit which was not designed with formal verification specifically in mind has been verified. They 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).
formal verification, Kapur-Narendran method, military image processing system, Sobel image processing chip, hardware verification, equational approach, n-bit adders, sequential circuits
Stillman and Narendran, "Formal verification of the Sobel image processing chip," Design Automation Conference(DAC), Anaheim, CA, USA, 1988, pp. 211-217.