6.3. Symbolic Simulation for Equivalence Checking

Symbolic simulation has become one of the most common techniques in hardware verification. Since variables in the descriptions are treated as symbols rather than as concrete-valued bit vectors, symbolic simulation can efficiently verify larger descriptions better than traditional logic simulation.

Here, we present a symbolic simulator for the equivalence checking of two C descriptions. The simulator is based on the method shown in Ritter [1], which verifies the equivalence of RTL or gate-level descriptions in HDL. We extend the method for the verification of C descriptions. The characteristics of the extended symbolic simulator are as follows: