Example - buffer allocation controller

This example is designed to control the allocation and freeing of buffers in, for example, a packet router. It will demonstrate how to embed assertions within Synchronous Verilog control constructs, such as if and while in order to specify temporal properties, without using temporal logic.

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 16, using a macro definition. We also need to define the log of this number, to indicate the number of bits in the buffer addresses.

`define SIZE 16
`define LOG_SIZE 4
module main(alloc,nack,alloc_addr,free,free_addr);
  input alloc;
  output nack;
  output [(`LOG_SIZE-1):0] alloc_addr;
  input free;        
  input [(`LOG_SIZE-1):0] free_addr;

  reg busy[0:(`SIZE - 1)];
  reg count[`LOG_SIZE:0];

  initial begin
    busy = 0;
    count = 0;
  end

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.

  always begin
    nack = alloc & (count == `SIZE);
    count = count + (alloc & ~nack) - (free & busy[free_addr]);
  end

Next we handle the setting and clearing of the busy bits:

  always begin
    if(free) busy[free_addr] = 0;
    if(alloc & ~nack) busy[alloc_addr] = 1;
  end

Note, that if a buffer is both freed and allocated at the same time, the net result is that its busy bit is set. Finally, we choose a buffer to allocate using a priority encoder. Our priority encoder is implemented as follows:

  always begin
    for(i = (`SIZE - 1); i >= 0; i = i - 1)
      if (~busy[i]) alloc_addr = i;
  end

Note, the entire for loop executes in zero time. Also, in the case when all buffers are busy, alloc_addr is not assigned, and thus remains undefined (since it is a wire, not a register).

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:

  wire [0:(`SIZE - 1)] allocd, freed;
  for(i = 0; i < `SIZE; i = i +1)
   always
      begin
        allocd[i] = alloc & ~nack & alloc_addr == i;
        freed[i] = free & free_addr == i;
      end

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 simply write a block of code that waits for the given buffer to be asserted, then while it is not freed, asserts that it must not be allocated again. At the end, when the buffer is freed, we also assert that it is not simultaneously allocated again. Note that we have given both these assertions the same label safe[i]. Thus, a failure in either case will cause a failure of safe[i].

  for(i = 0; i < `SIZE; i = i + 1)
    always begin
      if (allocd[i]) begin
        wait(1);
        while(~freed[i]) begin
          assert safe[i]: ~allocd[i];
          wait(1);
        end
        assert safe[i]: ~allocd[i];
      end
    end

Now, let's verify this specification. Open the file and verify the property safety[0]. It should be true. You might want to modify the code so that the counter is decremented whenever free is asserted (whether or not the busy bit is set for the freed buffer). If you try to verify this version you will find that in fact the property safety[0] false, and get a counterexample showing a case where the counter gets out of sync.