An approach for interpreted sequential verification
at different levels of abstraction by symbolic simulation is proposed.
Equivalence checking of two designs at rt-level using the symbolic simulator has
been presented in [21,20].
We describe in this paper the automatic verification of
gate-level results of a commercial synthesis tool against a behavioral
specification at rt-level. The symbolic simulator has to cope with
different numbers of control steps since the descriptions are not cycle
equivalent. The state explosion problem of previous approaches relying on
state traversal is avoided.\\
The simulator uses a library of different equivalence detection
techniques which are surveyed with main emphasis on techniques required at
gate-level. Cooperation of those techniques and good
debugging support are possible by notifying detected relationships at
equivalence classes rather than to manipulate symbolic terms.
