diff --git a/docs/examples/fifo/golden/fifo.sby b/docs/examples/fifo/golden/fifo.sby new file mode 100644 index 0000000..d94789c --- /dev/null +++ b/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 diff --git a/docs/examples/fifo/golden/fifo.sv b/docs/examples/fifo/golden/fifo.sv new file mode 100644 index 0000000..014563d --- /dev/null +++ b/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 diff --git a/docs/source/newstart.rst b/docs/source/newstart.rst index ebc443f..2828cb6 100644 --- a/docs/source/newstart.rst +++ b/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 `_, 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 ********************************* @@ -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: ## 0:00:00 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: ## 0:00:00 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: ## 0:00:00 Status: failed + SBY [fifo_nofullskip] engine_0.basecase: ## Assert failed in fifo: a_count_diff + SBY [fifo_nofullskip] engine_0.basecase: ## Assert failed in fifo: ap_underfill + 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 @@ -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: ## 0:00:00 Writing trace to VCD file: engine_0/trace2.vcd + 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/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 `. +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 `, +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 -with SystemVerilog Assertions. +immediate and concurrent assertions, refer to appnote 109: `Property Checking +with SystemVerilog Assertions +`_.