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 fr 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 data symmetric data type that allows adding and subtracting constants. 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 delcare a type as follows:
ordset TYPE 0..1000;then, in addition to the operations allowable on scalarset types, the following are also legal:
Induction is done in the following way: suppose we want to prove property p[i], where i is the induction paremeter, 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.
Decrementing is similary defined. Any property provable in this
abstract interpretation is provable in the original. In addition,
we can show that all the cases from i = 2 up to
i = 999 are isomorphic. Thus it is sufficient to prove
oly the cases i = 0, 1, 2, 1000.
As an example, suppose we hae 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 noncircular. Further, using its induction rule, it automatically generates a data type reduction using the values i and i-1, and it generates the four cases we need to prove: p[0], p[1], [2], p[1000]. To confirm this, run the example, and look in the properties ane. You should see the four aforementioned properties. Now choose Verify All to verify that in fact the induction works, and that p[i] holds for all i.