A buffer allocation controller

This example is designed to control the allocation and freeing of buffers in, for example, a packet router. The controller keeps an array of ``busy'' bits, one for each available data buffer. The busy bit is true when the buffer is in use, and false otherwise. An input alloc indicates a request to allocate a new buffer for use. If there is a buffer available, the controller outputs the index of this buffer on a signal alloc_addr. If there is no buffer available, it asserts an output nack. To make the circuit a little more interesting, we'll add a counter that keeps track of the number of busy bits that are set. Thus nack is asserted when the count is equal to the total number of buffers. To begin with, we'll define the number of buffers to be 32, using a C-style macro definition:

#define SIZE 32
module main(alloc,nack,alloc_addr,free,free_addr)
{
  input alloc : boolean;
  output nack : boolean;
  output alloc_addr : 0..(SIZE - 1);
  input free : boolean;
  input free_addr : 0..(SIZE - 1);

  busy : array 0..(SIZE - 1) of boolean;
  count : 0..(SIZE);

  init(busy) := [0 : i = 0..(SIZE-1)];
  init(count) := 0;

Note that we initialized busy to a vector of 32 zeros using an iterator expression. Here is the logic for the counter and the nack signal. Notice, we add one to the counter when there is an allocation request and nack is not asserted. We subtract one from the counter when there is a free request, and the buffer being freed is actually busy. Note, if we didn't check to see that the freed buffer is actually busy, the counter could get out of sync with the busy bits.

  nack := alloc & (count = SIZE);
  next(count) := count + (alloc & ~nack) - (free & busy[free_addr]);

Next we handle the setting and clearing of the busy bits. We use a default statement to indicate that, if a given buffer is being both freed and allocated at the same time, the allocation request takes precedence.

  default{
    if(free) next(busy[free_addr]) := 0;
  } in {
    if(alloc & ~nack) next(busy[alloc_addr]) := 1;
  }

Finally, we choose a buffer to allocate using a priority encoder. This is most easily generated using the chain constructor. This repeats a given block of statements for a range of index values, given precedence to later iterations. So, for example

    chain (i = 0; i < 3; i = i + 1) block(i)

is equivalent to

    default block(0) in default block(1) in default block(2)

Our priority encoder is defined as follows:

  chain(i = (SIZE - 1); i >= 0; i = i - 1){
    if(~busy[i]) alloc_addr := i;
  }

Since the last statement in the chain is the case i = 0, we effectively give highest priority to buffer  0. Note, in the case when all buffers are busy, alloc_addr in not assigned, and thus remains undefined.

Now, we consider the problem of specifying the buffer allocator. We will write a separate specification for each buffer, stating that the given buffer is never allocated twice without being freed in the interim. This is a technique known as ``decomposition'', that is, breaking a complex specification of a system into smaller parts that can be verified separately. To make it simpler to state the specification, it helps to define some additional signals: a bit allocd[i] to indicate that buffer i is currently being allocated, and a bit freed[i] to indicate that buffer i is currently being freed:

  for(i = 0; i < SIZE; i = i +1){
    allocd[i], freed[i] : boolean;

    allocd[i] := alloc & ~nack & alloc_addr = i;
    freed[i] := free & free_addr = i;
  }

Note, we used a for constructor to make an instance of these definitions for each buffer i. To write the specification that a buffer is not allocated twice, we can use ``until'' operator of temporal logic. Recall that the formula p U q in temporal logic means that q is eventually true, and until then, p must always be true.

  for(i = 0; i < SIZE; i = i +1){
    safe[i] : assert G (allocd[i] -> ~ X ((~freed[i]) U allocd[i]));
  }
}

Here we state that, if buffer i is allocated, then it is not the case that, starting at the next time, it remains unfreed until it is allocated a second time.

Now, let's verify this specification. Open the file and verify the property safety[0]. This should take something under a minute. If you watch the log output during the verification process, you'll notice that it is reporting a sequence of ``iterations''. These are the steps of a breadth-first search of the model's state space, starting from the initial states. The numbers reported are the sizes of the BDD's representing the set of states reached thus far in the search. The size of the BDD's can be much smaller than the number of states in the set. To see this, select ``Prop|State count''. This will rerun the verification and report the number of states reached at each iteration. The final number of states reached in this case is something over two billion.

Now let's increase the number of buffers from 32 to 64. Change the definition of SIZE at the beginning of the program to

#define SIZE 64

Open the new version, select the property safety[0], and then select ``Prop|State count''. This will verify the property, and also compute the number of states reached. You might want to go make a cup of coffee at this point, since the computation will take ten or twenty minutes. The only point to be made here is that the number of states reached is on the order of $10^{19}$, while the BDD representing this set of state has about 4000 ``nodes''. This shows that the BDD's can be a very compact representation for large sate sets. Sometimes, this makes it possible to verify a model, even though the number of states is much too large to be searched ``explicitly'' (i.e. larger than the number of atoms in the universe).

There is no guarantee, however, that SMV's BDD-based algorithms will be able solve a given verification problem. This is because the problem is SMV is trying to solve is fundamentally hard (PSPACE complete, to be precise). On the other hand, when SMV fails to solve a verification problem (or when we run out of patience waiting for it to solve the problem), there are usually many ways to make the problem simpler for SMV to solve. This usually involves decomposition - breaking big problems into small problems, and then localizing the verification of each subproblem to a small part of the overall model. This technique is described in the following section.