New exercise section

Worked exercise using the MAX_DATA parameter, highlighting its
incompleteness.  Includes completed examples in /golden subdirectory.

Also some formatting changes for spacing and extra links.

docs/examples/fifo/golden/fifo.sby

@@ -0,0 +1,32 @@
+[tasks]
+basic bmc
+nofullskip prove
+cover
+bigtest cover
+basic cover : default
+
+[options]
+cover:
+mode cover
+--
+prove:
+mode prove
+--
+bmc: 
+mode bmc
+--
+bigtest: depth 120
+~bigtest: depth 10
+
+[engines]
+smtbmc boolector
+
+[script]
+nofullskip: read -define NO_FULL_SKIP=1
+read -formal fifo.sv
+bigtest: hierarchy -check -top fifo -chparam MAX_DATA 100 -chparam ADDR_BITS 7
+~bigtest: hierarchy -check -top fifo -chparam MAX_DATA 5 -chparam ADDR_BITS 3
+prep -top fifo
+
+[files]
+fifo.sv

docs/examples/fifo/golden/fifo.sv

@@ -0,0 +1,192 @@
+// address generator/counter
+module addr_gen (
+    input en, clk, rst_n,
+    output reg [ADDR_BITS-1:0] addr
+);
+    parameter MAX_DATA = 16;
+    parameter ADDR_BITS = 5;
+
+    initial begin
+        addr <= 0;
+    end
+
+    // async reset
+    // increment address when enabled
+    always @(posedge clk or negedge rst_n) begin
+        if (~rst_n)
+            addr <= 0;
+        else if (en)
+            if (addr == MAX_DATA-1)
+                addr <= 0;
+            else
+                addr <= addr + 1;
+    end
+endmodule
+
+// Define our top level fifo entity
+module fifo (
+    input wen, ren, clk, rst_n,
+    input [7:0] wdata,
+    output [7:0] rdata,
+    output [ADDR_BITS:0] count,
+    output full, empty
+);
+    parameter MAX_DATA = 16;
+    parameter ADDR_BITS = 5;
+
+    // wire up our sub modules
+    // ADDR_BITS=5 gives 5 bits of address, [4:0]
+    // supporting MAX_DATA up to 2**5=32
+    wire [ADDR_BITS-1:0] waddr, raddr;
+    wire wskip, rskip;
+
+    // fifo storage
+    // reset not defined
+    reg [7:0] data [MAX_DATA-1:0];
+    always @(posedge clk) begin
+        if (wen) 
+            data[waddr] <= wdata;
+    end
+    assign rdata = data[raddr];
+
+    addr_gen #(.MAX_DATA(MAX_DATA), .ADDR_BITS(ADDR_BITS)) 
+    fifo_writer (
+        .en     (wen || wskip),
+        .clk    (clk  ),
+        .rst_n  (rst_n),
+        .addr   (waddr)
+    );
+
+    addr_gen #(.MAX_DATA(MAX_DATA), .ADDR_BITS(ADDR_BITS)) 
+    fifo_reader (
+        .en     (ren || rskip),
+        .clk    (clk  ),
+        .rst_n  (rst_n),
+        .addr   (raddr)
+    );
+
+    // internals
+    reg [ADDR_BITS:0] data_count;
+    initial begin
+        data_count <= 0;
+    end
+
+    always @(posedge clk or negedge rst_n) begin
+        if (~rst_n)
+            data_count <= 0;
+        else if (wen && !ren && data_count < MAX_DATA)
+            data_count <= data_count + 1;
+        else if (ren && !wen && data_count > 0)
+            data_count <= data_count - 1;
+    end
+
+    assign full  = data_count == MAX_DATA;
+    assign empty = (data_count == 0) && rst_n;
+    assign count = data_count;
+
+`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;
+`else
+    assign rskip = 0;
+    assign wskip = 0;
+`endif // NO_FULL_SKIP
+
+`ifdef FORMAL
+    // observers
+    wire [ADDR_BITS:0] addr_diff;
+    assign addr_diff = waddr >= raddr 
+                     ? waddr - raddr 
+                     : waddr + MAX_DATA - raddr;
+
+    reg init = 0;
+    always @(posedge clk) begin
+        if (rst_n)
+            init <= 1;
+        // if init is low we don't care about the value of rst_n
+        // if init is high (rst_n has ben high), then rst_n must remain high
+        assume (!init || init && rst_n);
+    end
+
+    // tests
+    always @(posedge clk) begin
+        if (rst_n) begin
+            // waddr and raddr can only be non zero if reset is high
+            w_nreset: cover (waddr || raddr);
+
+            // count never more than max
+            a_oflow:  assert (count <= MAX_DATA);
+            a_oflow2: assert (waddr < MAX_DATA);
+
+            // count should be equal to the difference between writer and reader address
+            a_count_diff: assert  (count == addr_diff 
+                                || count == MAX_DATA && addr_diff == 0);
+
+            // count should only be able to increase or decrease by 1
+            a_counts: assert (count == 0
+                            || count == $past(count)
+                            || count == $past(count) + 1
+                            || count == $past(count) - 1);
+
+            // read/write addresses can only increase (or stay the same)
+            a_raddr:  assert (raddr == 0
+                            || raddr == $past(raddr)
+                            || raddr == $past(raddr + 1));
+            a_waddr:  assert (waddr == 0
+                            || waddr == $past(waddr)
+                            || waddr == $past(waddr + 1));
+
+            // full and empty work as expected
+            a_full:  assert (!full || full && count == MAX_DATA);
+            w_full:  cover  (wen && !ren && count == MAX_DATA-1);
+            a_empty: assert (!empty || empty && count == 0);
+            w_empty: cover  (ren && !wen && count == 1);
+            
+            // can we corrupt our data?
+            w_overfill:  cover ($past(rskip) && raddr);
+            w_underfill: cover ($past(wskip) && waddr);
+        end else begin
+            // waddr and raddr are zero while reset is low
+            a_reset: assert (!waddr && !raddr);
+            w_reset: cover  (~rst_n);
+
+            // outputs are zero while reset is low
+            a_zero_out: assert (!empty && !full && !count);
+        end
+    end
+
+`ifdef VERIFIC
+    // if we have verific we can also do the following additional tests
+    always @(posedge clk) begin
+        if (rst_n) begin
+            // read/write enables enable
+            ap_raddr2: assert property (ren |=> $changed(raddr));
+            ap_waddr2: assert property (wen |=> $changed(waddr));
+
+            // read/write needs enable UNLESS full/empty
+            ap_raddr3: assert property (!ren && !full  |=> $stable(raddr));
+            ap_waddr3: assert property (!wen && !empty |=> $stable(waddr));
+                    
+            // can we corrupt our data?
+            ap_overfill:  assert property (wen && full  |=> $changed(raddr));
+            ap_underfill: assert property (ren && empty |=> $changed(waddr));
+            
+            // change data when writing (and only when writing) so we can line
+            // up reads with writes
+            assume property (wen |=> $changed(wdata));
+            assume property (!wen |=> $stable(wdata));
+        end
+    end
+`else // !VERIFIC
+    // without verific we are more limited in describing the above assumption
+    always @(posedge clk) begin
+        assume ((wen && wdata != $past(wdata)) 
+            || (!wen && wdata == $past(wdata)));
+    end
+`endif // VERIFIC
+
+`endif // FORMAL
+
+endmodule

docs/source/newstart.rst

@@ -3,9 +3,13 @@ Getting started
 ===============
 
 .. note:: 
+
     This tutorial assumes sby and boolector installation as per the 
     :ref:`install-doc`.  For this tutorial, it is also recommended to install 
     `GTKWave <http://gtkwave.sourceforge.net/>`_, an open source VCD viewer.
+    `Source files used in this tutorial
+    <https://github.com/YosysHQ/sby/tree/master/docs/examples/fifo>`_ can be 
+    found on the sby git, under ``docs/examples/fifo``.
 
 First In, First Out (FIFO) buffer
 *********************************
@@ -109,6 +113,7 @@ 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. 
 
@@ -139,12 +144,12 @@ following:
 
 .. code-block:: text
 
-    SBY [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Assert failed in fifo: a_count_diff
+    SBY [fifo_nofullskip] engine_0.basecase: ##  Assert failed in fifo: a_count_diff
-    SBY [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Assert failed in fifo: ap_underfill
+    SBY [fifo_nofullskip] engine_0.basecase: ##  Assert failed in fifo: ap_underfill
-    SBY [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
+    SBY [fifo_nofullskip] engine_0.basecase: ##  Writing trace to VCD file: engine_0/trace.vcd
-    SBY [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
+    SBY [fifo_nofullskip] engine_0.basecase: ##  Writing trace to Verilog testbench: engine_0/trace_tb.v
-    SBY [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
+    SBY [fifo_nofullskip] engine_0.basecase: ##  Writing trace to constraints file: engine_0/trace.smtc
-    SBY [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Status: failed
+    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
@@ -181,8 +186,8 @@ Searching the file for ``w_underfill`` will reveal the below.
 .. code-block:: text
 
     $ grep "w_underfill" fifo_cover/logfile.txt -A 1
-    SBY [fifo_cover] engine_0: ##   0:00:00  Reached cover statement at w_underfill in step 2.
+    SBY [fifo_cover] engine_0: ##  Reached cover statement at w_underfill in step 2.
-    SBY [fifo_cover] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace2.vcd
+    SBY [fifo_cover] engine_0: ##  Writing trace to VCD file: engine_0/trace2.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
@@ -193,7 +198,45 @@ write addresses and avoiding underflow.
 
 .. image:: media/gtkwave_coverskip.png
 
-For more on using the .sby file, see the :ref:`.sby reference page <Reference for .sby file format>`.
+Exercise
+********
+
+Adjust the ``[script]`` section of ``fifo.sby`` so that it looks like the below.
+
+.. code-block:: text
+
+    [script]
+    nofullskip: read -define NO_FULL_SKIP=1
+    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 :math:`2^4=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 :ref:`.sby reference page <Reference for .sby file format>`,
+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
 *********************
@@ -223,5 +266,6 @@ requires a skip in the read address, then the read address will *not* change.
 Further information
 *******************
 For more information on the uses of assertions and the difference between
-immediate and concurrent assertions, refer to appnote 109: Property Checking
+immediate and concurrent assertions, refer to appnote 109: `Property Checking
-with SystemVerilog Assertions.
+with SystemVerilog Assertions 
+<https://yosyshq.readthedocs.io/projects/ap109/en/latest/>`_.