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.