The disclosed design verification system includes a verification engine to model
the operation of an integrated circuit and to assess the model's adherence to a
property during N time steps of its operation. The value of N is recorded and propagated.
The propagated value of N is used to reduce resources expended during subsequent
analysis of the integrated circuit by ignoring the model's adherence to the property
during the early stages of subsequent analysis (during time steps less than N).
The system may include a diameter estimator that identifies a value of N beyond
which subsequent modeling of the integrated circuit produces no new states. Property
checking is ignored during states having a time step value greater than the estimated diameter.