Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders

This paper describes a new method that is useful in combinational equivalence checking with very challenging industrial designs. The method does not build a miter; instead it builds BDDs of reference and implementation circuits independently – so that each BDD can have its best order while building the BDD – then compares the two BDDs directly without transforming one variable order to the other. In the comparison, checking containment of two BDDs is necessary to handle don’t cares efficiently. Even though there are polynomial algorithms for checking equality of two BDDs, those algorithms are not extendible to containment checking. Thus we also present an efficient algorithm, of polynomial complexity, to check both equality and containment of two BDDs with different variable orders. Our non-miter-based method was able to verify many hard industrial designs previously infeasible with existing miter-based state-ofthe-art techniques. Experimental results show that the non-miter-ba...

• Type: Conference
• Year: 2004
• Where: FMCAD
• Authors: In-Ho Moon, Carl Pixley
• Keywords: Checking, FMCAD 2004, Industrial Designs, Variable Orders