Propagation of unknown values

To make its computations simpler, SMV sometimes uses an abstract ``unknown value'' to represent a value that is not completely determined. For example, if we write

  if(c) x := expr;

then, when the condition c is false, the value of x is undetermined (that is, it can be anything in the declared range of x). This is unfortunate, since if the value of x were completely determined by a given expression, SMV could simply substitute that expression for every occurrence of variable x, and thus avoid introducing a ``combinational variable'' for x when checking properties. In fact, if SMV were not able to make this substitution for most of the variables in a program, model checking even fairly small programs would be impossible. To make matters worse, in this case it is likely that we did not provide a ``default'' value for x because in fact we ``don't care'' about the value of x when c is false. Thus, to avoid introducing a combinational variable for x, SMV forces x to be deterministic by giving it the special value bottom as its default value. For those familiar with ``three valued'' logic simulators, this is very much like the ``X'' value in such a simulator. The value bottom appears in counterexample traces as a single dash ``-''.

The bottom value has a special property - replacing any value with bottom is a conservative abstraction in the sense that any property we can prove using this abstraction can be proved without it (though perhaps at a higher cost). Unfortunately, the converse is not true. That is, sometimes replacing the value of a variable with bottom, and thus avoiding a combinational variable, will lead to a false negative result. As a trivial example, suppose we tried to verify the property G (x = x). Clearly, this is a tautology, and should be true for any definition of x. However, in our case, if c is false, then by default x will get the value bottom. When evaluate bottom = bottom we get bottom (that is, it is unknown whether two unknown values are equal). In this case SMV's default abstraction is a bad one, since it prevents us from proving a property which is true.

The value bottom can arise in several other ways. For example, suppose that x and y are two variables of a scalarset type T, and we have reduced type T to just the value 0, and the abstract value NaN representing all the remaining values. If both x and y have the value NaN, then the expression x = y will yield bottom. That is, the truth value of the comparison might be either 0 or 1, but SMV represents both case by the single value bottom in order to avoid introducing a combinational variable for the choice. A similar case occurs when evaluating the expression a[x]. If x evaluates to NaN, then a[x] evaluates to bottom.

The most common way in which bottom values lead to problems is when they occur in the condition part of an if-then-else block. For example, suppose we had the following SMV program:

scalarset foo undefined;
module main(){
  x,y : foo;

  a,b : boolean;

  if(x=y){
    a := 0;
    b := 0;
  }
  else{
    a := 1;
    b := 1;
  }

  p : assert G (a = b);
}

Clearly, the property G (a=b) should be true, since if x = y then both are zero, and otherwise both are one. Try, however, to open this example and verify property p. SMV says it's false! In the counterexample, we see that x and y both have the value NaN, and as a result the value of the condition x=y is bottom. Thus, both a and b have the value bottom, and SMV cannot determine that they are equal. In fact, quite often, when SMV give a counterexample that looks nonsensical, you can trace it back to a bottom value occurring in a conditional.

SMV provides two ways to avoid this kind of problem. One is automatic but potentially costly, while the other is manual but less expensive. To solve the problem automatically, select Prop|Options from the menu pane and check the box that says ``Enumerate unknown values''. Now if you try again to verify the property, SMV should say it is true. In fact, SMV observed that the expression x=y might get the value bottom, and that this value might propagate into both variables a and b. Thus, it introduced a combinational variable for x=y. This in effect causes the model checker to enumerate both possible truth values of this expression. Since the property is true in both cases, this fixes the problem.

Unfortunately, using the ``Enumerate unknown values'' can cause a large number of combinational variables to be introduced, which can slow down the model checking process quite a lot (note, you won't see these added variables in the ``Cone'' pane, but they will be reported in the model checking transcript). In the case where the overhead resulting from ``Enumerate unknown values'' is unacceptable, it is also possible to introduce combinational variables manually for just those expressions that are causing problems. In the above case, for example, we could create a new boolean variable for the condition, as follows:

  c : boolean;
  c := (x=y);

  if(c){ ...

This by itself doesn't change anything. That is, since we have not explicitly asked for a nondeterministic choice in the value of c, SMV will by default give it the value bottom in the case when x=y is indeterminate. To tell SMV not to do this, and instead to make c a combinational variable, we can use the following statement:

  using enum(c) prove p;

This says to make c a combinational variable when proving p. If you open the modified version and verify p you can confirm that this also solves the problem. Ordinarily, if you think you are having problems with bottom values propagating too far, you should first try the ``Enumerate unknown values'' option. If that doesn't work however (either because of BDD explosion or because SMV still allowed bottom to propagate too far), then you can try the manual approach.