Sequential equivalence checking by symbolic simulation

An approach for interpreted sequential verification at different levels of abstraction by symbolic simulation is proposed. The equivalence checker has been used in previous work to compare two designs at rt-level. 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 the new 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.