Design Verification Based on Functional Abstraction

The aim of this report is to show the feasibility of automatic hardware verification based on functional abstraction. This is defined as the process of extracting the behavior of a product from its static structural description. A general discussion of possible approaches to design verification points out that functional abstraction is a very important part of any system for automatic hardware verification. Some of the tools developed for proofs of program correctness can be used when dealing with digital designs. In the present paper, the problems specific to hardware verification are singled out and investigated. Several tools specific to design verification, that were developed during the reported research, are briefly reviewed. The appendix begins with results of automatic analysis of basic modules (actual TTL components: flip-flops and an adder). These modules are then used in the realisation of more complex circuits. As an instructive example, three different designs implementing the same specifications are analyzed, and it is shown that the reported system is able to extract their common behavior.