Patent ID: 7512912

Claim:
A computer-readable storage medium storing instructions that when executed by a computer cause the computer to perform a method for determining a solution to a set of constraints during functional verification of a representation of an electronic design of an integrated circuit (IC), wherein the method comprises: generating a graph data structure representation for the set of constraints which includes both integer and Boolean constraints, comprising one or more nodes, each node having an associated range, wherein each node propagates one or more of Boolean values and non-Boolean values; and wherein the graph data structure is used to determine a solution set for the set of constraints simultaneously; wherein the range is comprised of a set of one or more intervals; and wherein a respective interval is a set of contiguous, monotonically increasing, integer values defined inclusively by a low value and a high value; solving both integer and Boolean constraints with a range-limiting method by: selecting a first decision variable; limiting a first range of the first decision variable to a first value; performing a first implication process, upon the ranges of the graph data structure, using the first range limitation; selecting a second decision variable, if no conflict resulted from the first implication process; and representing exclusion of the first value, from the first range, if a conflict resulted from the first implication process.