A circular buffer

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, recv_cell is the cell we are receiving a byte into, and send_cell is the cell we are sending a byte from. We block our input (setting inp.rrdy to zero) when the cell we are receiving into is full, and block our output (setting out.srdy to zero) when the cell we are sending from is empty. When we receive into a cell, we set its valid bit to true, and when we send from the cell, we clear its valid bit.

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 i, and the cell j that it is stored in. That way, we only need to consider one cell in the array at a time. Notice that adding ordering does not change the proof of data correctness in any way.

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 j = 0. In this case, the ``previous'' cell is cell 31. Since there's no way (yet) to write a special data type reduction for this case, we'll just include the value 31 in our data type reduction for all the cases. Thus, we write:

  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 ord_case[i-1] (for all cells) in this verification. This isn't really necessary, since only the ``previous cell'' (j-1 or 31) is needed in any give case, but its harmless. Note that we aren't doing induction over the cell number. In fact, we can't do this, since the cells are used in a circular manner. This would result in a cycle in the proof.

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.