Case analysis

Suppose that we have a condition p, and we would like to show that p holds true at all times. For any particular variable x, we could break the problem into cases. For each possible value of v of x, we could show that condition p is true at those times when x = v. Since at all times x must have one of these values, we can infer that p must be true at all times.

SMV has a special construct to support this kind of case analysis. It is especially useful for compositional verification, since for each case we can use a different abstraction of the system, including different components in the verification. This allows us to break large verification problems into smaller ones.

The above described case analysis is expressed in SMV in the following way:

  forall (v in TYPE)
    subcase q[v] of p for x = v;

Now suppose that p is some temporal assertion G cond, where cond is any boolean condition. The above declaration effectively defines a collection of properties q[v], as if we had written

  forall (x in TYPE)
    q[v] assert G (x=v -> cond);

That is, each q[v] asserts that p holds at those times when x = v. Clearly, if q[v] holds for all values of v, then p holds. Thus, SMV is relieved of the obligation of proving p, and instead separately proves all the cases of q[v]. Note that if TYPE is a scalarset type, we may in fact have to prove only one case, since all the other cases are symmetric.