Verification of relations between synchronous machines

The problem of implementation verification at the behavioral level is addressed. A formalism is needed for specifying synchronous circuits and expressing correctness requirements that leave room for modifying the input/output behavior of the implementation. Furthermore, a procedure is needed to verify these requirements. The authors model both specifications and implementations as synchronous logic circuits, and cast the correctness requirements as relations between string functions associated with a specification and an implementation. They define six primitive relations between string functions, namely delay, don´t care times, parallelism, encoding, input don´t care, and output don´t care relations. These relations have attributes, for instance, a delay time for the delay relation. It is shown that these relations can be verified by transforming the specification and the implementation and performing an input/output equivalence check. The authors also allow for composite relations, and show that, given an arbitrary composite relation, a closely related composition can be constructed which can be verified through one equivalence check. Experimental results are presented.<>