Combining Independent Cuts and Quantification for Equivalence Checking

In this paper, a novel algorithm is presented to enhance the effectiveness of the binary decision diagram(BDD) engine. It is proposed to select effective cut with no dependence remaining by using the circuit topology structure. And at the same time according to the heuristic information, we select more complex variables for quantification. Experimental results applied to ISCAS85 benchmark circuits demonstrate the practicability of our approach.