REACHABILITY-BASED VERIFICATION OF A CIRCUIT USING ONE OR MORE MULTIPLY ROOTED BINARY DECISION DIAGRAMS

In one embodiment, a method for reachability-based verification of a circuit using one or more multiply rooted binary decision diagrams (BDDs) includes generating a partitioned ordered BDD (POBDD) for one or more latches in the circuit and, 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 z. The method includes using each partition of the TR, performing a reachability-based analysis until one or more fixed points are reached.