Proof by induction

Suppose now that we want to verify some property of a long sequence. For example, we may have a counter in our design that counts up to a very large number. Such counters can lead to inefficient verification in SMV because the state space is very deep, and as a result, SMV's breadth first search technique requires a large number of iterations to exhaustively search the state space. However, the usual mathematic proof technique when dealing with long sequences is proof by induction. For example, we might prove that a property holds for 0 (the base case), and further that if it holds for some arbitrary value i, then it holds for i + 1. We then conclude by induction that the property holds for all i.

Data type reductions provide a mechanism for inductive reasoning in SMV. To do this, however, we need a symmetric data type that allows adding and subtracting constants, and inequality comparisons. In SMV, such data types are called ordsets. An ordset is just like a scalarset, except the restrictions on ordsets are slightly relaxed. If we declare a type as follows:

ordset TYPE 0..1000;

then, in addition to the operations allowable on scalarset types, the following are also legal:

1. x + 1 and x - 1,
2. x = 0 and x = 1000
3. x < y, x > y, x <= y and x >= y

where x and y are of type TYPE. That is, we can increment and decrement values of ordset types, compare them with the extremal values of the type, and test inequality.

Induction is done in the following way: suppose we want to prove property p[i], where i is the induction parameter, ranging over type TYPE. We use a data type reduction that maps TYPE onto a set of four values: X,i-1,i,Y. Here the symbolic value X abstracts all the values less that i-1, and Y abstracts all the values greater than i. Incrementing a value in this reduced type is defined as follows:

    X     + 1  =  {X,i-1}
    (i-1) + 1  =  i
    i     + 1  =  Y
    Y     + 1  =  Y

That is, adding one to a value less than i-1 will result in either i-1 or a value less that i-1 (actually, it is a little more complicated than this in the case of Y + 1, since adding one to Y could also overflow the type, giving an undefined result). Decrementing is similarly defined. Any property provable in this abstract model is provable in the original. In addition, we can show that all the cases from i = 1 up to i = 1000 are isomorphic (the case i = 0 is special, since in this case i-1 is undefined). Thus it is sufficient, for example, to prove only the cases i = 0, 1, or i = 0, 2, etc.

As an example, suppose we have a counter that starts from zero and increments once per clock cycle, up to 1000. We'd like to show that for any value i from 0 to 1000, the counter eventually reaches i. Here's how we might set this up:

ordset TYPE 0..1000;

module main()
{
  x : TYPE;

  /* the counter */

  init(x) := 0;
  next(x) := x + 1;

  /* the property */        

  forall(i in TYPE)
    p[i] : assert F (x = i);

  /* the proof */
  forall(i in TYPE)
    using p[i-1] prove p[i];

}

We prove each case p[i] using p[i-1]. That is, when proving the counter eventually reaches i, we assume that it eventually reaches i-1. (Note that technically, for the case i = 0, we are asking SMV to use p[-1], but since this doesn't exist, it is ignored).

SMV can verify that this proof is non-circular. Further, using its induction rule, it automatically generates a data type reduction using the values i and i-1, and it generates two representative cases to prove: p[0] and p[2].¹ To confirm this, run the example, and look in the properties pane. You should see the aforementioned properties. Now choose Verify All to verify that in fact the induction works, and that p[i] holds for all i.