Sequential Equivalence Checking by Symbolic Simulation

Gerd Ritter

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


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.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:37
Start Conference Manager
Conference Systems