Method and system for case-splitting on nodes in a symbolic simulation framework

1. A method for performing verification, said method comprising:

receiving a design;

determining a number of simulation cycles necessary to simulate said design for verification;

building for said design an intermediate binary decision diagram set containing one or more nodes representing one or more variables;

in response to building said intermediate binary decision diagram set, initializing a plurality of registers associated with said design with initial values;

creating a binary decision diagram variable for each input to said design;

performing verification of said design by evaluating a property of said intermediate binary decision diagram;

building for said design a subsequent intermediate binary decision diagram set containing one or more nodes representing one or more variables;

updating said plurality of registers with a set of next state function values;

case splitting upon a first fattest variable from among said one or more variables represented by said one or more nodes by setting said first fattest variable to a first value;

first cofactoring said intermediate binary decision diagram set with respect to said one or more nodes using an inverse of said first value to generate a first cofactored binary decision diagram set;

second cofactoring said intermediate binary decision diagram set with respect to said one or more nodes using said first value to generate a second cofactored binary decision diagram set;

in response to determining at least one simulation cycle remains, repeating said building for said design said subsequent intermediate binary decision diagram set; and

in response to determining that at least one simulation cycle does not remain, outputting results of said verification.

2. The method of claim 1 , further comprising performing verification of said design by evaluating a property of said first cofactored binary decision diagram set.

3. The method of claim 1 , further comprising storing said first cofactored binary decision diagram set on a stack.

4. The method of claim 1 , further comprising, in response to a size of said intermediate binary decision diagram set exceeding a size threshold, selecting for case-splitting said fattest variable from among said one or more variables represented by said one or more nodes.

5. The method claim 4 , wherein:

selecting for case-splitting fattest variable from among said one or more variables represented by said one or more nodes further comprises selecting for case-splitting a set of multiple fattest variables from among said one or more variables represented by said one or more nodes; and

said method further comprises repeating said first case-splitting, first cofactoring, and first performing steps on each of said set of multiple fattest variables from among said one or more variables represented by said one or more nodes.

6. The method of claim 1 , wherein:

said step of first case-splitting upon a fattest variable from among said one or more variables represented by said one or more nodes by setting said fattest variable to a primary value further comprises first case-splitting upon a fattest from among said one or more variables represented by said one or more nodes by setting said fattest variable from among said one or more variables represented by said one or more nodes to a primary value at an identified time step.

7. The method of claim 6 , further comprising:

backtracking to a time step of a last case-split;

cofactoring said selected first one of said one or more nodes by setting said fattest variable from among said one or more variables represented by said one or more nodes to a secondary value; and

performing a symbolic analysis of said selected first one of said one or more nodes with said secondary value.

8. The method of claim 1 , further comprising:

constraining a target binary decision diagram with at least one constraint.