Patent ID: 8863049

Claim:
A computer program product for constraining counterexamples, the computer program product comprising a non-transitory computer-readable storage medium containing computer program code for: receiving a counterexample trace comprising a plurality of signals of a circuit design, the counterexample trace illustrating a behavior of the circuit design that violates a property defined for the circuit design; applying one or more soft constraints to generate an updated counterexample trace, the soft constraints defining preferences to be satisfied by the updated counterexample trace, wherein applying the one or more soft constraints comprises: applying the one or more soft constraints to a first plurality of signal-cycle pairs of a signal; determining whether applying the one or more soft constraints to the first plurality of signal-cycle pairs of the signal still results in violation of the property; and responsive to determining that the property is not still violated, applying the one or more soft constraints to a second plurality of the signal-cycle pairs of the signal that is a sub-set of the first plurality of the signal-cycle pairs; and displaying the updated counterexample trace.