Integrating a Boolean satisfiability checker and BDDs for combinational equivalence checking

There has been much interest in techniques which combine the advantages of function-based methods, such as BDDs, with structure-based methods such as ATPG, for verifying the equivalence of combinational circuits. However, most existing efforts have focused on exploiting circuit similarity through use of learning and/or ATPG-based methods rather than on making the integration between BDDs and ATPG techniques efficient. This paper presents a new technique, where the focus is on improving the equivalence check itself, thereby making it more robust in the absence of circuit similarity. It is based on tight integration of a Boolean Satisfiability Checker with BDDs, whereby BDDs are effectively used to reduce both the problem size and the number of backtracks for the satisfiability problem. This methodology does not preclude exploitation of circuit similarity, when it exists, since the improved check can be easily incorporated as the inner loop of the well-known iterative framework involving search and replacement of internally equivalent nodes. We demonstrate the significance of our contributions with practical results on the ISCAS benchmark circuits.