An Equivalence Checking Method for C Descriptions based on Symbolic Simulation with Textual Differences

T. Matsumoto, H. Saito, and M. Fujita (Japan)


VLSI Design and CAD, Equivalence Checking, C-basedDesign, Symbolic Simulation


In this paper, an efficient equivalence checking method for two C descriptions is described. The equivalence of two C descriptions is proved by symbolic simulation. Symbolic simulation used in this paper can prove the equivalence of all of the variables in the descriptions. However, to ver ify the equivalence of all of the variables takes long time if large descriptions are given. Therefore, to improve the ver ification, our method identifies textual differences between descriptions. The identified textual differences are used to reduce the number of equivalence checking among vari ables. The proposed method is implemented in C language and evaluated at some C descriptions.

Important Links:

Go Back