On Complexity of Internal and External Equivalence Checking

We compare the complexity of "internal" and "external" equivalence checking. The former is meant for proving the correctness of a synthesis transformation by which circuit N₂ is obtained from circuit N₁. The latter is meant for proving that circuits N₁ and N₂ are functionally equivalent without making any explicit assumptions about the origin of N₁ and N₂. We describe logic synthesis procedures that can produce a circuit N₂ whose equivalence with the original circuit N₁, most likely, can not be efficiently proved by an external equivalence checker. On the other hand, there are internal equivalence checking procedures that easily prove that N₁ and N₂ are equivalent. We give experimental data showing that these logic synthesis procedures are not a mathematical curiosity but indeed can be used as a powerful method of logic optimization.