Combining Binary Decision Diagrams and Boolean Satisfiability for Equivalence Checking

A new combinational equivalence checking approach integrating Binary Decision Diagrams and Boolean Satisfiability is proposed.The algorithm works on the representation called And/Inverter Graph of the circuit.The BDD propogation and Circuit-based SAT Solver are applied in an intertwined manner to reduce the space of the miter circuit. If failed,CNF-based SAT Solver is used to solve the problem.The efficiency of the proposed approach is shown through its application on the LGsynth91 benchmark circuits.