Our talk addresses the problem of equivalence checking (EC) of combinational circuits. Our interest in this topic is twofold. First, EC is an important problem of formal verification. Second, EC proofs have a particular structure that current SAT-solvers with conflict driven learning fail to reproduce.

We present a new method of EC based on a generic technique called logic relaxation (LoR). LoR is meant for checking if a propositional formula $F$ has only "good" satisfying assignments specified by a design property. The essence of LoR is to relax $F$ into a formula $F^{rlx}$ and compute a set $S$ of assignments containing all assignments that satisfy $F^{rlx}$ but do not satisfy $F$. Set $S$ is built by a procedure called partial quantifier elimination. If all possible bad satisfying assignments are in $S$, formula $F$ has only good satisfying assignments and so the design property in question holds.

We argue that EC by LoR provides a comprehensive method for exploiting the structural similarity of circuits to be checked for equivalence. We also discuss the difference between LoR and SAT-solving with conflict driven learning in the context of EC.

Short bio: Eugene Goldberg worked as a researcher at Cadence Berkeley Labs for 11 years and at Northeastern University for 6 years. His research interests are in design of efficient algorithms for hardware/software verification and synthesis.