Patent ID: 7571403

Claim:
A method for verifying a circuit, the method comprising: generating by one or more computing systems, one or more partitions of a state space of a circuit, each partition being associated with a representation that has a size; initiating processing of each of the generated partitions using the representations of the generated partitions to verify the circuit; if, during the processing of the partition, the size of one of the representations of one of the generated partitions exceeds a first threshold: determining at least one splitting variable usable to generate two or more subpartitions from the partition, the splitting variable being determined according to a cost function; generating two or more subpartitions from the partition using the determined splitting variable, each of the subpartitions also being associated with a representation that has a size; initiating processing of each of the two or more subpartitions; and if, during processing of each of the subpartitions, the size of the representation of the subpartition exceeds a second threshold, generating further subpartitions from the subpartition to limit partition-representation size.