Constraints, abstraction, and verification

Abstract

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.