Equivalence Checking of Non-Binary Combinational Netlists

Equivalence checking is an integral part of the formal verification of ASIC to ensure that the constructed design flow meets the specifications. State-of-the-art techniques and heuristics are available for combinational equivalence checking restricted to binary netlists and do not work for netlists containing and propagating the "X" value. To accommodate the X-value, a 3-valued formal analysis has to be done which is computationally exponentially harder than its binary counterpart and can be a capacity challenge for the verification tool. X-value propagation becomes crucial for applications including low power equivalence checking under power shutoff and comparing a Register Transfer Level (RTL) design to a synthesized netlist. This paper introduces an algorithm for X-value equivalence checking using Binary Decision Diagrams (BDD) for combinational circuits. It extends the functionality of pre-existing formal verification tools available for binary netlists, to X-value netlists by introducing new variables to the BDD. The Colorado University Decision Diagram (CUDD) package has been used for BDD manipulation.