Automatic procedures for the behavioral verification of digital designs
Filip Van Aelten · 1992
This thesis introduces automatic procedures for the behavioral verification of digital designs. The procedures differ from theorem provers in that they are fully automatic. They differ from most current automatic verification procedures in two respects. First, they leave room for modifications to the input/output behavior of the implementation. Second, one set of procedures is compositional in nature allowing for the verification of larger designs than can be verified with most current automatic procedures. Both the implementation and the specification are taken to be finite state machines (FSM's), represented at the logic level, with an associated string function describing the input/output behavior. Correctness is taken to mean that one of a collection of relations holds between the string functions associated with the implementation and the specification. Fully general verification procedures for these relations are constructed from FSM equivalence checking algorithms, based on theorems which state necessary and sufficient conditions for correctness in terms of FSM equivalence. These procedures are applicable to small to medium-size circuits only. For large systems, compositional event-based procedures are developed which verify microcoded or array processors against signal flow graphs or dependency graphs. It is verified that the implementation has a satisfactory input/output behavior under the assumption that it executes the same set of operations as the specification. The compositional method is event-based and consists of verifying the combinational correctness of the data path modules in the implementation, and the validity of a collection of Computation Tree Logic (CTL) formulae on the controller. These constitute sufficient conditions for the validity of the $\beta$-relation between the implementation and the specification. Experimental results are presented. (Copies available exclusively from MIT Libraries, Rm. 14-0551, Cambridge, MA 02139-4307. Ph. 617-253-5668; Fax 617-253-1690.)