Verification of relations between synchronous machines
Filip Van Aelten, J. Allen, Srinivas Devadas · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · 1993
Uses string function theory to develop an efficient methodology for the verification of logic implementations against behavioral specifications. First, the authors define five primitive relations between string functions, other than strict automata equivalence, namely: don't care times, parallelism, encoding, input don't care and output don't care relations. These relations have attributes, For instance, the parallelism relation has an attribute corresponding to the degree of parallelism. For each of these primitive relations, the authors derive transformations on the specification and the implementation such that the relation holds between the specification and implementation if and only if the transformed circuits exhibit the same input/output behavior. This reduces the problem of verifying primitive relations to automata equivalence checking. They enlarge the set of relations between specifications and implementations by including arbitrary compositions of the five primitive relations. To reduce the cost of verifying such a composite relation, the authors show that, given an arbitrary composite relation, a fixed order composite relation can be constructed under certain assumptions), where the primitive relations occur at most once in a predetermined order, such that the original relation holds between two machines if and only if the fixed order relation holds. For the fixed order composite relation, they derive again transformations on the specification and the implementation which reduce verifying the composite relation to performing one equivalence check. The end result is a sound and complete proof method for proving arbitrary compositions of relations by transforming the specification and the implementation and performing an equivalence check on the transformed finite state machines.>