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 after 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 the previous techniques was capable of solving. The efficiency of the proposed approach is shown through its application on hard to prove industrial circuits and the ISCAS'85 benchmark circuits.