Method and system for combinational verification having tight integration of verification techniques

A computer-readable medium having computer instructions stored thereon for causing a processor performing a series of acts to determine whether first and second combinational netlists comprised of a plurality of nets and stored in a memory of a computer system are equivalent, the series of acts comprising:

• applying input vectors to the first and second netlists stored in the memory to generate cutpoint candidates from the nets in the netlists;
• resolving the cutpoint candidates to determine whether the cutpoint candidates are true cutpoints by selectively invoking, depending on whether the cutpoint candidates are likely to be true cutpoints, first and second resolution techniques;
• if the cutpoint candidates are not true cutpoints, generating a witness illustrating that the cutpoint candidates are not true cutpoints and refining the cutpoint candidates with the witness;
• and
• determining whether the first and second combinational netlists are equivalent based on results of the resolving act and the refining act.

A computer system for performing combinational verification of first and second netlists each comprising of a plurality of nets and stored in a memory of the computer system, the computer system comprising:

• an analysis module determining whether first and second nets respectively of the first and second netlists stored in the memory are likely to be equivalent;
• a BDD module for performing BDD composition of the first and second nets if the nets are likely to be equivalent to determine whether the nets are equivalent;
• a satisfiability module for performing satisfiability analysis of the first and second nets if the nets are not likely to be equivalent to determine whether the nets are equivalent;
• a passing module for passing information about the first and second nets between the BDD and the satisfiability modules if either the BDD module or the satisfiability module fails to determine whether the nets are equivalent;
• and
• a switch module for invoking the BDD module with the passed information if the satisfiability module fails to determine whether the nets are equivalent and for invoking the satisfiability module with the passed information if the BDD module fails to determine whether the nets are equivalent.

A method of performing satisfiability analysis on a set of m root and p cutpoint BDDs representing a pair of cutpoint candidate BDDs stored in a memory of a computer system to determine whether the pair of cutpoint candidate BDDs are equivalent, the method comprising the steps of:

• simplifying the set of m root and p cutpoint BDDs;
• assigning random values to variables in the m root and p cutpoint BDDS;
• calculating a first cost of a first one of the pair of cutpoint candidate BDDS and a second cost of a second one of the pair of cutpoint candidate BDDs from the random values of the variables in the m root and p cutpoint BDDs;
• and
• determining whether the pair of cutpoint candidate BDDs are equivalent based on the first cost and the second cost.

A method of determining whether a first netlist and a second netlist stored in a memory of a computer system are equivalent, the method comprising the steps of:

• dividing cutpoint candidates in the first and second netlists stored in the memory into a plurality of classes;
• resolving cutpoint candidates within a class of the plurality of classes to determine whether the cutpoint candidates are equivalent, the resolving step comprising the steps of:
• performing a first type of cutpoint resolution on the class of cutpoint candidates in response to the cutpoint candidates being likely to be equivalent;
• performing a second type of cutpoint resolution on the class of cutpoint candidates in response to the cutpoint candidates being not likely to be equivalent;
• invoking the second type of cutpoint resolution with information learned by the first type of cutpoint resolution in response to the first type of cutpoint resolution not resolving the cutpoint candidates;
• and
• invoking the first type of cutpoint resolution with information learned by the second type of cutpoint resolution in response to the second type of cutpoint resolution not resolving the cutpoint candidates;
• and
• generating an indication demonstrating an inequivalency in response to the cutpoint candidates being inequivalent.

A computer system for performing combinational verification of a first netlist and a second netlist, each comprising a plurality of nets and stored in a memory of the computer system, the computer system comprising:

• an analysis module determining whether a first net of the first netlist and a second net of the second netlist are likely to be equivalent;
• a BDD module performing a BDD composition of the first net and the second net to determine whether the first net and the second net are equivalent in response to the first net and the second net being likely to be equivalent;
• and
• a satisfiability module performing a satisfiability analysis of the first and second nets to determine whether the first net and the second net are equivalent in response to the first net and the second net being unlikely to be equivalent.