22. The apparatus of claim 17 , wherein the second subset of assumptions is an under-approximation of the first set of assumptions.
17. An apparatus for verifying a circuit design, comprising: an association mechanism configured to: simplify a first set of assumptions to obtain a second set of assumptions, wherein the second set of assumptions is logically equivalent to the first set of assumptions, and wherein first set of assumptions and the second set of assumptions are correspond to allowable input assignments for the circuit design; and associate a first subset of assumptions with an assertion in a set of assertions, wherein the first subset of assumptions is a subset of the second set of assumptions, and wherein satisfying the assertion corresponds to a desired behavior of circuit design; an approximation mechanism configured to modify the first subset of assumptions to obtain a second subset of assumptions which is not logically equivalent to the first subset of assumptions; and a formal verification mechanism configured to prove that the circuit design satisfies the assertion when the second subset of assumptions is satisfied.