Exploiting suspected redundancy for enhanced design verification

A computer program product comprising computer executable instructions, stored on a computer readable medium for verifying an original model of an integrated circuit, the original model being described by a netlist including a set of gates and a set of edges representing interconnections between the gates, comprising:

• computer code means for proposing an equivalence class comprised of a set of candidate gates suspected of exhibiting equivalent behavior;
• computer code means for creating a set of equivalence gates, wherein an equivalence gate comprises an XOR or XNOR product of a representative gate and a selected one of the candidate gates;
• computer code means for creating a speculatively reduced netlist by replacing the representative gate as the source gate for edges sourced by the selected candidate gate;
• and
• computer code means for performing additional verification on the speculatively reduced netlist wherein the additional verification is selected from the group consisting of:
• verifying formally the equivalence of the gates in the equivalence class including applying a plurality of transformation engines to the speculatively reduced netlist;
• and
• performing incomplete search to yield verification coverage data and, for the duration of the incomplete search for which none of the equivalence gates is asserted, applying verification coverage results derived from said duration of the incomplete search to the original model.

A verification system including processor, system memory, and storage, comprising,

• means for proposing an equivalence class comprised of a set of candidate gates suspected of exhibiting equivalent behavior;
• means for identifying one of the candidate gates as a representative gate for the equivalence class;
• means for creating a set of equivalence gates, wherein an equivalence gate comprises an XOR or XNOR product of the representative gate and one of the candidate gates;
• means for creating a speculatively reduced netlist by replacing the representative gate as the source gate for edges sourced by a candidate gate;
• and
• means for performing additional verification on the speculatively reduced netlist wherein the additional verification is selected from the group consisting of:
• verifying formally the equivalence of the gates in the equivalence class including applying a plurality of transformation engines to the speculatively reduced netlist;
• and
• performing incomplete search to yield verification coverage data and, for the duration of the incomplete search for which none of the equivalence gates is asserted, applying verification coverage results derived from said duration of the incomplete search to the original model.