An automata-theoretic approach to behavioral equivalence

The problem of verifying the equivalence of a behavioral description against a logic-level implementation is addressed. One major hindrance toward a precise notion of behavioral verification has been that parallel, serial or pipelined implementations of the same behavioral description can be implemented in finite-state automata with different input/output behaviors. The authors use nondeterminism to model the degree of freedom that is afforded by parallelism in a behavioral description that also contains complex control. Given some assumptions, they show how the set of finite automata derivable from a behavioral description can be represented compactly as an input-programmed automaton (p-Automaton), i.e., an automaton with programmed meta-input variables. The logic-level implementation is deemed to be equivalent to the behavioral description if and only if the p-Automaton is equivalent to the logic-level finite automaton under some assignment to the meta-input variables. The method allows for extending the use of finite-state automata equivalence-checking algorithms to the problem of behavioral verification.<>