Techniques are disclosed for automatically determining whether a potential
constraint set to be applied to a portion of a circuit are
overconstrained. An environment circuit supplies inputs to the circuit
portion. Embodiments of the invention recognize that if the environment
circuit produces a set of outputs that contain a pattern that is not
present in the potential constraint set, then the potential constraint
set is overconstrained. A verification tool establishes the properties
for the environmental circuit based on the potential constraint set. If
the verification tool determines that the outputs produced by the
environment circuit conflict with the properties of the environment
circuit, then the verification tool concludes that the potential
constraint set is overconstrained, because the environment circuit
produces a pattern that is not present in the potential constraint set.
Advantageously, the laborious and error-prone process of manually
determining the proper inputs to apply during formal verification is
avoided.