On Complexity of Equivalence Checking
Cadence Berkeley Labs, Yakov Novikov · 2003
We introduce the notion of a common specification (CS) that is the key to understanding the complexity of equivalence checking. A CS S of functionally equivalent Boolean circuits N 1 and N 2 is a circuit of multi-valued blocks where N 1 and N 2 can be obtained from this CS by encoding the values of multi-valued variables of S. We show that the performance of an equivalence checking algorithm heavily depends on whether a non-trivial CS S is known. If it is, then there exists an algorithm we describe whose run time is linear in the number of blocks in S. However, there are good reasons to believe that for any algorithm that does not have information about such a CS, equivalence checking is hard (if not infeasible). We experimentally show that even equivalence checking of circuits with a very fine CS is hard for a representative collection of methods while CS driven equivalence checking takes only a few seconds.