Equivalence Checking Using Trace Partitioning

One application of equivalence checking is to establish correspondence between a high-level, abstract design and a low-level implementation. We propose a new partitioning technique for the case in which the two designs are substantially different and traditional equivalence-point insertion fails. The partitioning is performed in tandem in both models, exploiting the structure present in the high-level model. The approach generates many but tractable SAT/SMT queries. We present experimental data quantifying the benefit of our partitioning method for both combinational and sequential equivalence checking of difficult arithmetic circuits and control-intensive circuits.