Here, I discuss some results on
equivalence checking (**EC**) of circuits with a common specification. These
results provide a strong evidence that **external **EC is **unsolvable **even
for combinational circuits and even in “a practical sense”. I call EC external if it is performed
by an outsider i.e. if no information is provided about the circuits *N* and *N*^{*}
to be checked for equivalence other than circuit description. From a
practical point of view, this means that

·
Efficient external EC of *N* and *N*^{*}
is possible only if

· these circuits are narrow, i.e. have small width and so have compact BDDs,

· or "almost identical" e.g. they have a lot of functionally equivalent internal points.

·
On the contrary, **internal **EC i.e. EC
where some extra information is provided about the relation between *N*
and *N*^{*} can be efficient even if external EC is not.

· A logic synthesis tool should preserve some constraints (like toggle equivalence, see below) guaranteeing that EC can be done efficiently. Similarly, a compiler parses a string of symbols based on a grammar , which, in a sense, is a bunch of constraints, rather than tries to understand this string according to some ever-growing set of heuristics.

Below, I describe some results on EC and
explain my point of view in the Q&A session. Some
questions are "real" and were asked explicitly or implicitly by
reviewers and some I made up myself. (*This is work in progress. I am going
to add new questions and answers in the future *.)

The formulation of the EC problem can be found in [1]. Here, I discuss the "simplest version" of EC, namely the EC of combinational circuits.

Here is the main idea. Let *N* and *N*^{*} be two
single-output combinational circuits to be checked for equivalence. Let *N*
and *N*^{*} be partitioned into subcircuits *N*_{1},...,
*N*_{k} and *N*^{*}_{1},...,*N*^{*}_{k}
respectively so that

- subcircuits
*N*_{i}and*N*^{*}_{i}are connected in the same way in*N*and*N*^{*} - corresponding
subcircuits
*N*_{i}and*N*^{*}_{i}are toggle equivalent

A partition of *N* into subcircuits *N*_{i}
is called a specification of *N* (denoted as *Spec*(*N*)).
Circuits *N* and *N*^{*} are said to have a **common
specification** if subcircuits *N*_{i} and *N*^{*}_{i},
*i*=1,..,*k* satisfy the two conditions above.

Let circuits *M* and *M ^{*}* have identical sets of input
variables.

Importantly, circuits *N* and *N*^{*} with a common
specification can be **efficiently checked for equivalence** if
specifications of *N* and *N*^{*} are known. The
corresponding EC procedure can be found, for example, in [2]).
(We will refer to this procedure as **EC_TE** where EC stands for
Equivalence Checking and TE stands for Toggle Equivalence). The EC_TE procedure
is linear in the number of subcircuits in *Spec*(*N*) and *Spec*(*N ^{*}*)
and exponential in the

Along with paper [7], we call EC **external **if no
extra information about circuits *N* and *N*^{*} to be
checked for equivalence is given. Otherwise, EC is called **internal **. So
the EC_TE procedure is internal because *Spec*(*N*) and *Spec*(*N ^{*}*)
provide extra knowledge about

**Q.** How do your
results relate to state-of-the-art EC?

**A.** In a sense, EC of circuits *N* and *N ^{*}* with a
common specification (and EC in general) can be viewed as a "decryption process".
Here

**Q.**
Are these results of any practical importance? Current
logic synthesis algorithms do not produce circuits with a common specification

**A.** The main point is that the complexity of EC and power of logic
synthesis are tightly related. The more perturbed an initial circuit *N*
is by logic synthesis, the harder it is to prove the equivalence of *N*
and the optimized circuit *N ^{*}* without any additional
information.

In [2], we sketch a powerful logic synthesis procedure
enabled by EC_TE. Given a circuit *N* and its partition into subcircuits *N*_{1},...,*N*_{k}
(i.e. its specification),this procedure builds an optimized circuit *N*^{*}
with the same specification as *N*. We will refer to this procedure as
LS_TE (here LS stands for Logic Synthesis and TE for Toggle Equivalence). LS_TE
builds circuit *N*^{*} by replacing subcircuits *N*_{i}
of *Spec*(*N*) with toggle equivalent counterparts *N*^{*}_{i}
in topological order. Importantly, LS_TE has the same complexity as EC_TE that
is it is linear in the number of subcircuits *N*_{i} and
exponential in the granularities of *Spec*(*N*) and *Spec*(*N*^{*}).
So if the granularity of *Spec*(*N*) is bounded by a constant (this essentially
means that granularity of *Spec*(*N*^{*}) is also bounded by
a constant), then LS_TE is linear in circuit size and so it is scalable. On the
other hand, LS_TE enjoys great flexibility because the number of subcircuits
toggle equivalent to *N*_{i} is astronomical even if the number of
outputs in*N*_{i} is small. (Let a subcircuit *N*_{i}
has *k* outputs. Then the number of, say, *k* output Boolean
functions toggle equivalent to the function implemented by *N*_{i}
is, roughly speaking, 2^{k}!. For k=5 this number is equal to 2.6 × 10^{35}.
In [5], we describe a procedure that, given a subcircuit *N*_{i}
builds an optimized toggle equivalent subcircuit *N*^{*}_{i}.
This procedure, makes LS_TE "a reality".

In [6], we show that LS_TE can be viewed as a way to
address the local minima entrapment problem. The depth of the minimum that can
be (potentially) escaped depends on the granularity of *Spec*(*N*).
The larger this granularity is, the deeper local minimum can be escaped.

**Q.**
How does the claim that EC is "unsolvable" is
different from a well-known fact that EC is coNP-complete and so, most
probably, it can not be solved efficiently in the general case?

**A.** The fact that a particular class of EC problems is hard to solve may
mean two things. First, circuits *N* and *N ^{*}* of this
class are very different from each other and so there is no short proof (in a
particular proof system) that they are functionally equivalent. In this case,
EC is "naturally" hard. Second, circuits

Note that the very existence of these two types of complexity is still an open question. If NP=coNP, the first type of complexity does not exist for EC problems. (In this case, there should exist a powerful enough proof system in which all EC problems have short proofs.) However, the second kind of complexity still remains even if NP=coNP (because short proofs may be exponentially hard to find) and "disappears" only if P = NP (in which case not only all EC problems should have short proofs, but there should exist an efficient algorithm for finding such proofs).

*Wikipedia. Article on equivalence checking.*- E.Goldberg.
*On Equivalence Checking and Logic Synthesis of Circuits with a Common Specification.*GLSVLSI-2005. - C.L.Berman.
*Circuit width, register allocation, and ordered binary decision diagrams.*IEEE Trans. on CAD. Vol 10:8, 1991, pp.1059-1066. - R.Braynt.
*Graph-Based Algorithms for Boolean Function Manipulation.*IEEE Transactions on Computers. Vol. C-35, No. 8, August, 1986, pp. 677-691. - E.Goldberg,K.Gulati,S.Khatri.
*Toggle Equivalence Preserving (TEP) logic synthesis*, DSD-2007,Lubeck, Germany - E.Goldberg.
*Escaping Local Minima in Logic Synthesis*, IWLS-2007,San Diego 2007. - E.Goldberg,K.Gulati.
*On Complexity of External and Internal Equivalence Checking.*DSD-2007,Lubeck, Germany