An Equivalence Checking Method for Circuits with Black Boxes Based on Logic Cone and SAT

In this paper, an approach has been proposed for solving this problem of equivalence checking for partial implementation in digital circuits. The partial implementation can also be called Black Boxes in which parts of the implementation are not yet finished or known. First, the reference and partial implementation designs are divided into small components called logic cones respectively; Second, logic cones are matched using matching techniques between reference and partial implementation designs; Third, an “exclusive-or” logic gate is applied to the two matched logic cones to construct a miter; Finally, each miter is proven to be functionally equivalent or nonequivalent using SAT engine. The method of circuit partition is used to equivalence checking for partial implementations in order to decrease the time and space complexity. A series of experimental results show the effectiveness and feasibility of the approach on the ISCAS´85 benchmark circuits.