In one embodiment, a method for directed falsification of a circuit includes selecting a partition of a state space of the circuit. The partition includes only a portion of the state space and is selected according to one or more results of one or more preimage calculations indicating one or more characteristics of the circuit. The characteristics indicate a likelihood that the partition includes one or more errors in the circuit. The method further includes, using one or more partitioned ordered binary decision diagrams (POBDDs), analyzing the partition according to a falsification-based forward-reachability technique to determine whether the partition includes one or more errors in the circuit.