Reachability-based verification of a circuit using one or more multiply rooted binary decision diagrams

1. A system for reachability-based verification of a circuit using one or more multiply rooted binary decision diagrams (BDDs), the system comprising:

a partitioned ordered BDD (POBDD) module operable to generate a POBDD for one or more latches in the circuit;

a transition relation (TR) module operable, for each POBDD, to:

graph a TR associated with the POBDD that reflects a plurality of input and state variables for the POBDD;

generate two disjunctive partitions of the POBDD;

compare the two disjunctive partitions with a threshold;

if the two disjunctive partitions are below the threshold, assign the POBDD to the root of a noncube-based partitioning tree (NCPT) that comprises a plurality of leaves; and

for each leaf of the NCPT, compose one or more decomposition points and generate one or more partitions; and

an analysis module operable:

using each partition of the TR, to perform a reachability-based analysis until one or more fixed points are reached;

to communicate a result of the reachability-based analysis for reachability-based verification of the circuit.

2. The system of claim 1 , wherein, for each leaf of the NCPT, all decomposition points are composed and all partitions are generated.

3. The system of claim 1 , wherein a POBDD is generated for every latch in the circuit.

4. The system of claim 1 , wherein a TR is graphed by composing one or more decomposition points until the TR blows up.

5. The system of claim 1 , wherein the threshold is a predefined threshold.

6. The system of claim 1 , wherein a size of each of the two disjunctive partitions is compared with the threshold, the size of each of the two disjunctive partitions being determined according to a number of new allocated nodes.

7. The system of claim 1 , wherein the TR module is further operable, if the two disjunctive partitions are not below the threshold, to use one or more cube-based partitioning techniques to reduce the POBDD.

8. The system of claim 1 , wherein a first POBDD is operable to communicate with one or more other POBDDs using a generalized cofactor operation.

9. A method for reachability-based verification of a circuit using one or more multiply rooted binary decision diagrams (BDDs), the method comprising:

generating a partitioned ordered BDD (POBDD) for one or more latches in the circuit;

for each POBDD:

graphing a transition relation (TR) associated with the POBDD that reflects a plurality of input and state variables for the POBDD;

generating two disjunctive partitions of the POBDD;

comparing the two disjunctive partitions with a threshold;

if the two disjunctive partitions are below the threshold, assigning the POBDD to the root of a noncube-based partitioning tree (NCPT) that comprises a plurality of leaves; and

for each leaf of the NCPT, composing one or more decomposition points and generating one or more partitions;

using each partition of the TR, performing a reachability-based analysis until one or more fixed points are reached; and

communicating a result of the reachability-based analysis for reachability-based verification of the circuit.

10. The method of claim 9 , wherein, for each leaf of the NCPT, all decomposition points are composed and all partitions are generated.

11. The method of claim 9 , wherein a POBDD is generated for every latch in the circuit.

12. The method of claim 9 , wherein a TR is graphed by composing one or more decomposition points until the TR blows up.

13. The method of claim 9 , wherein the threshold is a predefined threshold.

14. The method of claim 9 , wherein a size of each of the two disjunctive partitions is compared with the threshold, the size of each of the two disjunctive partitions being determined according to a number of new allocated nodes.

15. The method of claim 9 , further comprising, if the two disjunctive partitions are not below the threshold, using one or more cube-based partitioning techniques to reduce the POBDD.

16. The method of claim 9 , wherein a first POBDD is operable to communicate with one or more other POBDDs using a generalized cofactor operation.

17. Logic for reachability-based verification of a circuit using one or more multiply rooted binary decision diagrams (BDDs), the logic encoded in media and when executed operable to:

generate a partitioned ordered BDD (POBDD) for one or more latches in the circuit;

for each POBDD:

graph a transition relation (TR) associated with the POBDD that reflects a plurality of input and state variables for the POBDD;

generate two disjunctive partitions of the POBDD;

compare the two disjunctive partitions with a threshold;

if the two disjunctive partitions are below the threshold, assign the POBDD to the root of a noncube-based partitioning tree (NCPT) that comprises a plurality of leaves; and

for each leaf of the NCPT, compose one or more decomposition points and generate one or more partitions;

using each partition of the TR, perform a reachability-based analysis until one or more fixed points are reached; and

communicate a result of the reachability-based analysis for reachability-based verification of the circuit.

18. The logic of claim 17 , wherein, for each leaf of the NCPT, all decomposition points are composed and all partitions are generated.

19. The logic of claim 17 , wherein a POBDD is generated for every latch in the circuit.

20. The logic of claim 17 , wherein a TR is graphed by composing one or more decomposition points until the TR blows up.

21. The logic of claim 17 , wherein the threshold is a predefined threshold.

22. The logic of claim 17 , wherein a size of each of the two disjunctive partitions is compared with the threshold, the size of each of the two disjunctive partitions being determined according to a number of new allocated nodes.

23. The logic of claim 17 , further operable, if the two disjunctive partitions are not below the threshold, to use one or more cube-based partitioning techniques to reduce the POBDD.

24. The logic of claim 17 , wherein a first POBDD is operable to communicate with one or more other POBDDs using a generalized cofactor operation.

25. A system for reachability-based verification of a circuit using one or more multiply rooted binary decision diagrams (BDDs), the system comprising:

means for generating a partitioned ordered BDD (POBDD) for one or more latches in the circuit;

means for, for each POBDD:

graphing a transition relation (TR) associated with the POBDD that reflects a plurality of input and state variables for the POBDD;

generating two disjunctive partitions of the POBDD;

compare the two disjunctive partitions with a threshold;

if the two disjunctive partitions are below the threshold, assigning the POBDD to the root of a noncube-based partitioning tree (NCPT) that comprises a plurality of leaves; and

for each leaf of the NCPT, composing one or more decomposition points and generating one or more partitions;

using each partition of the TR, perform a reachability-based analysis until one or more fixed points are reach; and

communication a result of the reachability-based analysis for reachability-based verification of the circuit.