Now let's consider transmission of an infinite sequence of bytes again, but this time using our array of cells as a circular buffer (an implementation of a FIFO queue).

To begin with, we need to add handshaking to our interface definition,
so add the following to module `byte_intf`:

srdy, rrdy : boolean; valid := srdy & rrdy;

The signal `srdy` indicates that the sender is ready,
while `rrdy` indicates the the receiver is ready.
The data are valid, by definition, when both are ready.

Now, as in section 4.5, we'll use an array of 32 cells, to hold our data items. So define the type CELL as:

ordset CELL 0..31;

The reason for making it an `ordset` type will become
apparent later. Now, replace the previous ``trivial''
implementation with the following:

cells : array CELL of struct{ valid : boolean; idx : INDEX; data : BYTE; } recv_cell, send_cell : CELL; inp.rrdy := ~cells[recv_cell].valid; out.srdy := cells[send_cell].valid; forall(i in CELL)init(cells[i].valid) := 0; default{ if(inp.valid){ next(cells[recv_cell].valid) := 1; next(cells[recv_cell].idx) := inp.idx; next(cells[recv_cell].data) := inp.data; } } in { if(out.valid){ next(cells[send_cell].valid) := 0; } } out.idx := cells[send_cell].idx; out.data := cells[send_cell].data;Note,

Up to this point, we haven't said what policy is used to choose
`recv_cell` and `send_cell`. To make our buffer ordered,
we can use a round-robin policy. This means that each time we
receive a byte, we increment `recv_cell` by one, and each time
we send a byte, we increment `send_cell` by one. When either
of these reaches its maximum value, it returns to zero. To accomplish
this, add to following code to the implementation:

init(recv_cell) := 0; if(inp.srdy & inp.rrdy) next(recv_cell) := (recv_cell = 31) ? 0 : recv_cell +1; init(send_cell) := 0; if(out.srdy & out.rrdy) next(send_cell) := (send_cell = 31) ? 0 : send_cell +1;

Note that, since `CELL` is an ordset type, rather than a `scalarset`, it's legal to compare it against the maximum value (31)
and set it back to the minimum value (0). If `CELL` were a scalarset,
it wouldn't be legal to introduce any constants of the type.

Now that we have our implementation, lets prove both the correctness of the data output and correctness of the ordering. The case splitting statement for data correctness is the same as when we did this example in section 4.6.2, where we weren't concerned with data ordering:

forall(i in INDEX) forall(j in CELL) subcase spec_case[i][j] of out.data//spec for out.idx = i & send_cell = j;That is, we consider separately the case of each byte index

Now for the ordering question. Again, we are going to use induction.
The ordering property says that when the output data are valid, the
output index must be equal to are count of the number of previous
values. We'll do the proof by induction over the value of the counter.
That is, we'll assume that the index was correct when the count was
`i-1`, and then prove that the index is correct when the count is `i`.
This means that, as before, we have to split cases based on `cnt`.
However, in this case we also have to split cases on the cell in which
the current output value stored. Thus, we use the following case
splitting declaration:

forall(i in INDEX) forall(j in CELL) subcase ord_case[i][j] of out.ordered for out.cnt = i & send_cell = j;

Now, the question is, what data type reduction to use for type `CELL`.
We know we need to use cell `j`, since that is the one holding the
data item we are interested in. However, in addition, we need to use the
previous cell. The intuition behind this is as follows. We are assuming
that the output index is correct for byte `i-1`. If byte `i` is
stored in cell `j`, then byte `i-1` is stored in cell `j-1`
(which one exception). This means we need to include cell `j-1`. Then,
if cell `j-1` contains index i-1, and the inputs are ordered, it
follows that cell `j` will contain index `i`, which is what we
are trying to prove. Thus, we might use the data type reduction:

CELL -> {j-1..j}However, note that the exception to the above reasoning is the case

forall(i in INDEX) forall(j in CELL) using CELL -> {j-1..j,31} prove ord_case[i][j];

Now comes the actual inductive step: we use the case `cnt = i-1`
to prove the case `cnt = i`:

forall(i in INDEX} forall(j in CELL) using ord_case[i-1], inp.ordered prove ord_case[i][j]; assume inp.ordered;Notice that we use the entire array

Now, run this
example, and note the properties
that appear in the properties pane. You'll observe that the
property `ord_case[i][j]` has to be proved for all the combinations
of `i = 0,2` and `j = 0,2,31`. The reason we have extra cases
to prove for the cell index `j`, is that we included the maximum
value `31` in the data type reduction. SMV reasons that the
case `j=31` might not be isomorphic to the other cases, since
we might compare `j` in some way with the value 31. However,
as you can observe by selecting ``Prop|Verify All'', all of these
cases can be verified quickly. This is because the number of state variables is
small after data type reductions.

Thus, we've proved that a circular buffer implementation correctly transmits an infinite sequence of bytes using a given handshake protocol.