Patent ID: 7280993

Claim:
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.