Incremental formal design verification

Abstract

Language containment is a method for design verification that involves checking if the behavior of the system to be verified is a subset of the behavior of the specifications (properties or requirements), which it has to meet. If this check fails, language containment returns a subset of “fair” states involved in behavior that the system exhibits but the specification does not. Current techniques for language containment do not take advantage of the fact that the process of design is incremental; namely that the designer repeatedly modifies and re-verifies his/her design. This results in unnecessary and cumbersome computation. We present a method, which successively modifies the latest result of verification each time the design is modified. Our incremental algorithm translates changes made by the designer to an addition or subtraction of edges, states or constraints (on acceptable behavior) from the transition behavior or specification of the problem. Next, these changes are used to update the set of “fair” states previously computed. This incremental algorithm is superior to the current techniques for language containment; a conclusion supported by the experimental results presented in this paper.