Combinational equivalence checking using Boolean Satisfiability and Binary Decision Diagrams

Most recent combinational equivalence checking techniques are based on exploiting circuit similarity. In this paper, we focus on circuits with no internal equivalent nodes or alter internal equivalent nodes have been identified and merged. We present a new technique integrating Boolean Satisfiability and Binary Decision Diagrams. The proposed approach is capable of solving verification instances that neither of both techniques was capable to solve. The efficiency of the proposed approach is shown through its application on hard to prove industrial circuits and the ISCAS'85 benchmark circuits.