A method for verifying a property associated with a target circuit is provided
that includes receiving information associated with a target circuit, the information
identifying a property within the target circuit to be verified. One or more partitioned
ordered binary decision diagram (POBDD) operations are then executed using the
information in order to generate a first set of states at a first depth associated
with a sub-space within the target circuit. Bounded model checking may be executed
using the first set of states in order to generate a second set of states at a
second depth associated with the sub-space within the target circuit. The first
set of states may be used as a basis for the second set of states such that the
second depth is greater than the first depth.
