Constraints, abstraction, and verification.

Circuits are not designed to work in all environments: a contract exists between a circuit and the environments in which it correctly operates. The contract is specified by constraints, predicates that must be satisfied by the inputs supplied to the circuit by its environment. A verifier employs contraints during verification to ignore behaviors that will not arise. This paper systematically investigates constraints. We show that: the standard verification condition needs to be revamped to avoid technical and philosophical problems; that there are two important classes of constraints; that one of these classes can be automatically generated; and that constraints arise from an interaction between models and abstractions. [ABSTRACT FROM AUTHOR]