Getting started

Note

This tutorial assumes sby and boolector installation as per the Installation guide. For this tutorial, it is also recommended to install GTKWave, an open source VCD viewer. Source files used in this tutorial can be found on the sby git, under docs/examples/fifo.

First In, First Out (FIFO) buffer

From Wikipedia, a FIFO is

a method for organizing the manipulation of a data structure (often, specifically a data buffer) where the oldest (first) entry, or “head” of the queue, is processed first.

Such processing is analogous to servicing people in a queue area on a first-come, first-served (FCFS) basis, i.e. in the same sequence in which they arrive at the queue’s tail.

In hardware we can create such a construct by providing two addresses into a register file. This tutorial will use an example implementation provided in fifo.sv.

First, the address generator module:

// address generator/counter
module addr_gen 
#(  parameter MAX_DATA=16
) ( input en, clk, rst,
    output reg [3:0] addr
);
    initial addr <= 0;

    // async reset
    // increment address when enabled
    always @(posedge clk or posedge rst)
        if (rst)
            addr <= 0;
        else if (en) begin
            if (addr == MAX_DATA-1)
                addr <= 0;
            else
                addr <= addr + 1;
        end
endmodule

This module is instantiated twice; once for the write address and once for the read address. In both cases, the address will start at and reset to 0, and will increment by 1 when an enable signal is received. When the address pointers increment from the maximum storage value they reset back to 0, providing a circular queue.

Next, the register file:

// fifo storage
// async read, sync write
wire [3:0] waddr, raddr;
reg [7:0] data [MAX_DATA-1:0];
always @(posedge clk)
    if (wen) 
        data[waddr] <= wdata;
assign rdata = data[raddr];

Notice that this register design includes a synchronous write and asynchronous read. Each word is 8 bits, and up to 16 words can be stored in the buffer.

Verification properties

In order to verify our design we must first define properties that it must satisfy. For example, there must never be more than there is memory available. By assigning a signal to count the number of values in the buffer, we can make the following assertion in the code:

a_oflow:  assert (count <= MAX_DATA);

It is also possible to use the prior value of a signal for comparison. This can be used, for example, to ensure that the count is only able to increase or decrease by 1. A case must be added to handle resetting the count directly to 0, as well as if the count does not change. This can be seen in the following code; at least one of these conditions must be true at all times if our design is to be correct.

a_counts: assert (count == 0
               || count == $past(count)
               || count == $past(count) + 1
               || count == $past(count) - 1);

As our count signal is used independently of the read and write pointers, we must verify that the count is always correct. While the write pointer will always be at the same point or after the read pointer, the circular buffer means that the write address could wrap around and appear less than the read address. So we must first perform some simple arithmetic to find the absolute difference in addresses, and then compare with the count signal.

assign addr_diff = waddr >= raddr 
                 ? waddr - raddr 
                 : waddr + MAX_DATA - raddr;

a_count_diff: assert (count == addr_diff 
                   || count == MAX_DATA && addr_diff == 0);

SymbiYosys

SymbiYosys (sby) uses a .sby file to define a set of tasks used for verification.

basic

Bounded model check of design.

nofullskip

Demonstration of failing model using an unbounded model check.

cover

Cover mode (testing cover statements).

noverific

Test fallback to default Verilog frontend.

The use of the :default tag indicates that by default, basic and cover should be run if no tasks are specified, such as when running the command below.

sby fifo.sby

Note

The default set of tests should all pass. If this is not the case there may be a problem with the installation of sby or one of its solvers.

To see what happens when a test fails, the below command can be used. Note the use of the -f flag to automatically overwrite existing task output. While this may not be necessary on the first run, it is quite useful when making adjustments to code and rerunning tests to validate.

sby -f fifo.sby nofullskip

The nofullskip task disables the code shown below. Because the count signal has been written such that it cannot exceed MAX_DATA, removing this code will lead to the a_count_diff assertion failing. Without this assertion, there is no guarantee that data will be read in the same order it was written should an overflow occur and the oldest data be written.

`ifndef NO_FULL_SKIP
    // write while full => overwrite oldest data, move read pointer
    assign rskip = wen && !ren && data_count >= MAX_DATA;
    // read while empty => read invalid data, keep write pointer in sync
    assign wskip = ren && !wen && data_count == 0;
`endif // NO_FULL_SKIP

The last few lines of output for the nofullskip task should be similar to the following:

SBY [fifo_nofullskip] engine_0.basecase: ##  Assert failed in fifo: a_count_diff
SBY [fifo_nofullskip] engine_0.basecase: ##  Writing trace to VCD file: engine_0/trace.vcd
SBY [fifo_nofullskip] engine_0.basecase: ##  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY [fifo_nofullskip] engine_0.basecase: ##  Writing trace to constraints file: engine_0/trace.smtc
SBY [fifo_nofullskip] engine_0.basecase: ##  Status: failed
SBY [fifo_nofullskip] engine_0.basecase: finished (returncode=1)
SBY [fifo_nofullskip] engine_0: Status returned by engine for basecase: FAIL
SBY [fifo_nofullskip] engine_0.induction: terminating process
SBY [fifo_nofullskip] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:02 (2)
SBY [fifo_nofullskip] summary: Elapsed process time unvailable on Windows
SBY [fifo_nofullskip] summary: engine_0 (smtbmc boolector) returned FAIL for basecase
SBY [fifo_nofullskip] summary: counterexample trace: fifo_nofullskip/engine_0/trace.vcd
SBY [fifo_nofullskip] DONE (FAIL, rc=2)
SBY The following tasks failed: ['nofullskip']

Using the noskip.gtkw file provided, use the below command to examine the error trace.

gtkwave fifo_nofullskip/engine_0/trace.vcd noskip.gtkw

This should result in something similar to the below image. We can immediately see that data_count and addr_diff are different. Looking a bit deeper we can see that in order to reach this state the read enable signal was high in the first clock cycle while write enable is low. This leads to an underfill where a value is read while the buffer is empty and the read address increments to a higher value than the write address.

During correct operation, the w_underfill statement will cover the underflow case. Examining fifo_cover/logfile.txt will reveal which trace file includes the cover statment we are looking for. If this file doesn’t exist, run the code below.

sby fifo.sby cover

Searching the file for w_underfill will reveal the below.

$ grep "w_underfill" fifo_cover/logfile.txt -A 1
SBY [fifo_cover] engine_0: ##  Reached cover statement at w_underfill in step 2.
SBY [fifo_cover] engine_0: ##  Writing trace to VCD file: engine_0/trace4.vcd

We can then run gtkwave with the trace file indicated to see the correct operation as in the image below. When the buffer is empty, a read with no write will result in the wksip signal going high, incrementing both read and write addresses and avoiding underflow.

gtkwave fifo_cover/engine_0/trace4.vcd noskip.gtkw

Note

Implementation of the w_underfill cover statement depends on whether Verific is used or not. See the Concurrent assertions section for more detail.

Exercise

Adjust the [script] section of fifo.sby so that it looks like the below.

[script]
nofullskip: read -define NO_FULL_SKIP=1
noverific: read -noverific
read -formal fifo.sv
hierarchy -check -top fifo -chparam MAX_DATA 17
prep -top fifo

The hierarchy command we added changes the MAX_DATA parameter of the top module to be 17. Now run the basic task and see what happens. It should fail and give an error like Assert failed in fifo: a_count_diff. Can you modify the verilog code so that it works with larger values of MAX_DATA while still passing all of the tests?

Note

If you need a hint, try increasing the width of the address wires. 4 bits supports up to 2⁴=16 addresses. Are there other signals that need to be wider? Can you make the width parameterisable to support arbitrarily large buffers?

Once the tests are passing with MAX_DATA=17, try something bigger, like 64, or 100. Does the basic task still pass? What about cover? By default, bmc & cover modes will run to a depth of 20 cycles. If a maximum of one value can be loaded in each cycle, how many cycles will it take to load 100 values? Using the .sby reference page, try to increase the cover mode depth to be at least a few cycles larger than the MAX_DATA.

Note

Reference files are provided in the fifo/golden directory, showing how the verilog could have been modified and how a bigtest task could be added.

Concurrent assertions

Until this point, all of the properties described have been immediate assertions. As the name suggests, immediate assertions are evaluated immediately whereas concurrent assertions allow for the capture of sequences of events which occur across time. The use of concurrent assertions requires a more advanced series of checks.

Compare the difference in implementation of w_underfill depending on the presence of Verific. w_underfill looks for a sequence of events where the write enable is low but the write address changes in the following cycle. This is the expected behaviour for reading while empty and implies that the w_skip signal went high. Verific enables elaboration of SystemVerilog Assertions (SVA) properties. Here we use such a property, write_skip.

property write_skip;
    @(posedge clk) disable iff (rst)
    !wen |=> $changed(waddr);
endproperty
w_underfill: cover property (write_skip);

This property describes a sequence of events which occurs on the clk signal and are disabled/restarted when the rst signal is high. The property first waits for a low wen signal, and then a change in waddr in the following cycle. w_underfill is then a cover of this property to verify that it is possible. Now look at the implementation without Verific.

reg past_nwen;
initial past_nwen <= 0;
always @(posedge clk) begin
    if (rst) past_nwen <= 0;
    if (!rst) begin
        w_underfill: cover (past_nwen && $changed(waddr));
        past_nwen <= !wen;
    end
end

In this case we do not have access to SVA properties and are more limited in the tools available to us. Ideally we would use $past to read the value of wen in the previous cycle and then check for a change in waddr. However, in the first cycle of simulation, reading $past will return a value of X. This results in false triggers of the property so we instead implement the past_nwen register which we can initialise to 0 and ensure it does not trigger in the first cycle.

As verification properties become more complex and check longer sequences, the additional effort of hand-coding without SVA properties becomes much more difficult. Using a parser such as Verific supports these checks without having to write out potentially complicated state machines. Verific is included for use in the Tabby CAD Suite.

Further information

For more information on the uses of assertions and the difference between immediate and concurrent assertions, refer to appnote 109: Property Checking with SystemVerilog Assertions.