On equivalence checking and logic synthesis of circuits with a common specification

ABSTRACT. In this paper we develop a theory of equivalence checking (EC) and logic synthesis of circuits with a common specification (CS). We show that two combinational circuits N 1, N 2 have a CS iff they can be partitioned into subcircuits that are connected “in the same way ” and are toggle equivalent. This fact allows one to represent a specification of a circuit implicitly as a partitioning into subcircuits. We give an efficient procedure for checking if circuits N 1, N 2 have the same predefined specification. As a “by-product”, this procedure performs EC of N 1 and N 2. We show how, given a circuit N 1 with a predefined specification, one can efficiently build a circuit N 2 satisfying the same specification. We give experimental evidence that EC of N 1, N 2 is hard if their CS is unknown