Method and system for equivalence-checking combinatorial circuits using interative binary-decision-diagram sweeping and structural satisfiability analysis

A computer program product for use with a design workstation, wherein said computer program product comprises signal bearing media containing program instructions for execution on said workstation for comparing a first logical circuit to a second logical circuit by performing the steps of:

• constructing a combined circuit graph representing said first circuit and said second circuit, wherein said combined circuit graph includes a plurality of nodes;
• computing a binary decision diagram (BDD) for one of said plurality of nodes within said combined circuit graph;
• merging said node if said BDD is already present on a heap;
• storing said BDD on said heap if said BDD is not already present on said heap;
• determining whether or not a size of a smallest BDD on said heap has exceeded a predetermined lower size limit;
• in response to a determination that said size of said smallest BDD has not exceeded said predetermined lower size limit, repeating said steps of computing, merging, storing and determining;
• and
• in response to a determination that said size of said heap has exceeded said predetermined lower size limit, analyzing said first circuit and said second circuit using a satisfiability analysis to detect conflicts between values that can be assumed by said plurality of nodes.

A workstation comprising:

• a memory subsystem for storing operands and data;
• means for processing a series of program instructions for comparing a first logical circuit to a second logical circuit by performing the steps of:
• constructing a combined circuit graph representing said first circuit and said second circuit, wherein said combined circuit graph includes a plurality of nodes;
• computing a binary decision diagram (BDD) for one of said plurality of nodes within said combined circuit graph;
• merging said node if said BDD is already present on a heap;
• storing said BDD on said heap if said BDD is not already present on said heap;
• determining whether or not a size of a smallest BDD on said heap has exceeded a predetermined lower size limit;
• in response to a determination that said size of said smallest BDD has not exceeded said predetermined lower size limit, repeating said steps of computing, merging, storing and determining;
• and
• in response to a determination that said size of said heap has exceeded said predetermined lower size limit, analyzing said first circuit and said second circuit using a satisfiability analysis to detect conflicts between values that can be assumed by said plurality of nodes.