Incremental formal design verification
Gitanjali Swamy, Robert K. Brayton · 1994
Design verification is the processof ensuring that a designedsystem satisfies its original requirements. Language containment, a method for performing design verification, involves checking if the behavior of the system to be verified is a subset of the behavior of the specifications(properties or requirements). If the language containment condition is not met then the process returns a subset of states involved in behavior that the system exhibits but the specification does not. This subset is called the set of `Bad' or `Fair' states and they are used to indicate that the system failed verification. In practice, the process of design is incremental and the designer repeatedly modifies and re-verifies his/her design. Current techniques for language containment do not take advantage of this, resulting in unnecessary recomputation that can be cumbersome if small changes are made to a large system. We present an alternate method, which takes advantage of the incremental nature of the desi...