The present invention provides methods and systems for using a design
element in a graphical model to represent and identify a precondition for
use by a verification tool in verifying an executable form of the design
represented by the graphical model. The precondition design element
provides a specification of a verification constraint without affecting
the behavior of the design. The constraint is to be applied by the
verification tool in verifying the design. As such, the precondition
design element of the present invention provides a mechanism and
formalism in a model-based design approach that is used to constrain
automatically generated tests or verification of the design represented
by the graphical model.