mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-27 23:45:50 +00:00
Code Activity

Merge pull request #174 from KrystalDelusion/fifo_example

Browse source
This commit is contained in:
N. Engelhardt 2022-08-22 11:34:51 +02:00 • committed by GitHub
commit 4adb99ea30
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
14 changed files with 864 additions and 205 deletions
Download patch file Download diff file Expand all files Collapse all files

1
docs/examples/fifo/.gitignore vendored Normal file
View file

@ -0,0 +1 @@
fifo_*/

3
docs/examples/fifo/Makefile Normal file
View file

@ -0,0 +1,3 @@
SUBDIR=../docs/examples/fifo
TESTDIR=../../../tests
include $(TESTDIR)/make/subdir.mk

29
docs/examples/fifo/fifo.sby Normal file
View file

@ -0,0 +1,29 @@
[tasks]
basic bmc
nofullskip prove
cover
noverific cover
basic cover : default
[options]
cover:
mode cover
--
prove:
mode prove
--
bmc:
mode bmc
--
[engines]
smtbmc boolector
[script]
nofullskip: read -define NO_FULL_SKIP=1
noverific: read -noverific
read -formal fifo.sv
prep -top fifo
[files]
fifo.sv

13
docs/examples/fifo/fifo.sh Normal file
View file

@ -0,0 +1,13 @@
#!/bin/bash
python3 $SBY_MAIN -f fifo.sby basic cover noverific
if [[ $? -ne 0 ]] ; then
exit 1
fi
python3 $SBY_MAIN -f fifo.sby nofullskip
if [[ $? -ne 2 ]] ; then
exit 1
fi

197
docs/examples/fifo/fifo.sv Normal file
View file

@ -0,0 +1,197 @@
// 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
// Define our top level fifo entity
module fifo
#( parameter MAX_DATA=16
) ( input wen, ren, clk, rst,
input [7:0] wdata,
output [7:0] rdata,
output [4:0] count,
output full, empty
);
wire wskip, rskip;
reg [4:0] data_count;
// 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];
// end storage
// addr_gen for both write and read addresses
addr_gen #(.MAX_DATA(MAX_DATA))
fifo_writer (
.en (wen || wskip),
.clk (clk ),
.rst (rst),
.addr (waddr)
);
addr_gen #(.MAX_DATA(MAX_DATA))
fifo_reader (
.en (ren || rskip),
.clk (clk ),
.rst (rst),
.addr (raddr)
);
// status signals
initial data_count <= 0;
always @(posedge clk or posedge rst) begin
if (rst)
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;
assign count = data_count;
// overflow protection
`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 [4:0] addr_diff;
assign addr_diff = waddr >= raddr
? waddr - raddr
: waddr + MAX_DATA - raddr;
// tests
always @(posedge clk) begin
if (~rst) begin
// waddr and raddr can only be non zero if reset is low
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 || count == MAX_DATA);
w_full: cover (wen && !ren && count == MAX_DATA-1);
a_empty: assert (!empty || count == 0);
w_empty: cover (ren && !wen && count == 1);
// reading/writing non zero values
w_nzero_write: cover (wen && wdata);
w_nzero_read: cover (ren && rdata);
end else begin
// waddr and raddr are zero while reset is high
a_reset: assert (!waddr && !raddr);
w_reset: cover (rst);
// outputs are zero while reset is high
a_zero_out: assert (!empty && !full && !count);
end
end
`ifdef VERIFIC
// if we have verific we can also do the following additional tests
// read/write enables enable
ap_raddr2: assert property (@(posedge clk) disable iff (rst) ren |=> $changed(raddr));
ap_waddr2: assert property (@(posedge clk) disable iff (rst) wen |=> $changed(waddr));
// read/write needs enable UNLESS full/empty
ap_raddr3: assert property (@(posedge clk) disable iff (rst) !ren && !full |=> $stable(raddr));
ap_waddr3: assert property (@(posedge clk) disable iff (rst) !wen && !empty |=> $stable(waddr));
// use block formatting for w_underfill so it's easier to describe in docs
// and is more readily comparable with the non SVA implementation
property write_skip;
@(posedge clk) disable iff (rst)
!wen |=> $changed(waddr);
endproperty
w_underfill: cover property (write_skip);
// look for an overfill where the value in memory changes
// the change in data makes certain that the value is overriden
let d_change = (wdata != rdata);
property read_skip;
@(posedge clk) disable iff (rst)
!ren && d_change |=> $changed(raddr);
endproperty
w_overfill: cover property (read_skip);
`else // !VERIFIC
// implementing w_underfill without properties
// can't use !$past(wen) since it will always trigger in the first cycle
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
// end w_underfill
// w_overfill does the same, but has been separated so that w_underfill
// can be included in the docs more cleanly
reg past_nren;
initial past_nren <= 0;
always @(posedge clk) begin
if (rst) past_nren <= 0;
if (!rst) begin
w_overfill: cover (past_nren && $changed(raddr));
past_nren <= !ren;
end
end
`endif // VERIFIC
`endif // FORMAL
endmodule

34
docs/examples/fifo/golden/fifo.sby Normal file
View file

@ -0,0 +1,34 @@
[tasks]
basic bmc
nofullskip prove
cover
noverific cover
bigtest cover
[options]
cover:
mode cover
--
prove:
mode prove
--
bmc:
mode bmc
--
bigtest: depth 120
~bigtest: depth 10
nofullskip: expect fail
[engines]
smtbmc boolector
[script]
nofullskip: read -define NO_FULL_SKIP=1
noverific: read -noverific
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

198
docs/examples/fifo/golden/fifo.sv Normal file
View file

@ -0,0 +1,198 @@
// address generator/counter
module addr_gen
#( parameter MAX_DATA=16,
parameter ADDR_BITS=5
) ( input en, clk, rst,
output reg [ADDR_BITS-1: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
// Define our top level fifo entity
module fifo
#( parameter MAX_DATA=16,
parameter ADDR_BITS=5
) ( input wen, ren, clk, rst,
input [7:0] wdata,
output [7:0] rdata,
output [ADDR_BITS:0] count,
output full, empty
);
wire wskip, rskip;
reg [ADDR_BITS:0] data_count;
// fifo storage
// async read, sync write
wire [ADDR_BITS-1:0] waddr, raddr;
reg [7:0] data [MAX_DATA-1:0];
always @(posedge clk)
if (wen)
data[waddr] <= wdata;
assign rdata = data[raddr];
// end storage
// addr_gen for both write and read addresses
addr_gen #(.MAX_DATA(MAX_DATA), .ADDR_BITS(ADDR_BITS))
fifo_writer (
.en (wen || wskip),
.clk (clk ),
.rst (rst),
.addr (waddr)
);
addr_gen #(.MAX_DATA(MAX_DATA), .ADDR_BITS(ADDR_BITS))
fifo_reader (
.en (ren || rskip),
.clk (clk ),
.rst (rst),
.addr (raddr)
);
// status signals
initial data_count <= 0;
always @(posedge clk or posedge rst) begin
if (rst)
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;
assign count = data_count;
// overflow protection
`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;
// tests
always @(posedge clk) begin
if (~rst) begin
// waddr and raddr can only be non zero if reset is low
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 || count == MAX_DATA);
w_full: cover (wen && !ren && count == MAX_DATA-1);
a_empty: assert (!empty || count == 0);
w_empty: cover (ren && !wen && count == 1);
// reading/writing non zero values
w_nzero_write: cover (wen && wdata);
w_nzero_read: cover (ren && rdata);
end else begin
// waddr and raddr are zero while reset is high
a_reset: assert (!waddr && !raddr);
w_reset: cover (rst);
// outputs are zero while reset is high
a_zero_out: assert (!empty && !full && !count);
end
end
`ifdef VERIFIC
// if we have verific we can also do the following additional tests
// read/write enables enable
ap_raddr2: assert property (@(posedge clk) disable iff (rst) ren |=> $changed(raddr));
ap_waddr2: assert property (@(posedge clk) disable iff (rst) wen |=> $changed(waddr));
// read/write needs enable UNLESS full/empty
ap_raddr3: assert property (@(posedge clk) disable iff (rst) !ren && !full |=> $stable(raddr));
ap_waddr3: assert property (@(posedge clk) disable iff (rst) !wen && !empty |=> $stable(waddr));
// use block formatting for w_underfill so it's easier to describe in docs
// and is more readily comparable with the non SVA implementation
property write_skip;
@(posedge clk) disable iff (rst)
!wen |=> $changed(waddr);
endproperty
w_underfill: cover property (write_skip);
// look for an overfill where the value in memory changes
// the change in data makes certain that the value is overriden
property read_skip;
@(posedge clk) disable iff (rst)
!ren && d_change |=> $changed(raddr);
endproperty
w_overfill: cover property (read_skip);
`else // !VERIFIC
// implementing w_underfill without properties
// can't use !$past(wen) since it will always trigger in the first cycle
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
// end w_underfill
// w_overfill does the same, but has been separated so that w_underfill
// can be included in the docs more cleanly
reg past_nren;
initial past_nren <= 0;
always @(posedge clk) begin
if (rst) past_nren <= 0;
if (!rst) begin
w_overfill: cover (past_nren && $changed(raddr));
past_nren <= !ren;
end
end
`endif // VERIFIC
`endif // FORMAL
endmodule

28
docs/examples/fifo/noskip.gtkw Normal file
View file

@ -0,0 +1,28 @@
[*]
[*] GTKWave Analyzer v3.4.0 (w)1999-2022 BSI
[*] Thu Jun 09 02:02:01 2022
[*]
[timestart] 0
[size] 1000 320
[pos] -1 -1
*-3.253757 18 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 246
[signals_width] 200
[sst_expanded] 1
[sst_vpaned_height] 58
@28
fifo.clk
@22
fifo.data_count[4:0]
fifo.addr_diff[4:0]
@28
fifo.ren
fifo.wen
@22
fifo.raddr[3:0]
fifo.waddr[3:0]
@28
fifo.rskip
fifo.wskip
[pattern_trace] 1
[pattern_trace] 0

5
docs/source/index.rst
View file

@ -10,11 +10,6 @@ formal tasks:
* Unbounded verification of safety properties
* Generation of test benches from cover statements
* Verification of liveness properties
* Formal equivalence checking [TBD]
* Reactive Synthesis [TBD]
(Items marked [TBD] are features under construction and not available
at the moment.)
.. toctree::
:maxdepth: 3

195
docs/source/install.rst
View file

@ -1,9 +1,40 @@
Installing
==========
.. _install-doc:
Follow the instructions below to install SymbiYosys and its dependencies.
Yosys, SymbiYosys, and Z3 are non-optional. The other packages are only
required for some engine configurations.
Installation guide
==================
This document will guide you through the process of installing sby.
CAD suite(s)
************
Sby (SymbiYosys) is part of the `Tabby CAD Suite
<https://www.yosyshq.com/tabby-cad-datasheet>`_ and the `OSS CAD Suite
<https://github.com/YosysHQ/oss-cad-suite-build>`_! The easiest way to use sby
is to install the binary software suite, which contains all required
dependencies, including all supported solvers.
* `Contact YosysHQ <https://www.yosyshq.com/contact>`_ for a `Tabby CAD Suite
<https://www.yosyshq.com/tabby-cad-datasheet>`_ Evaluation License and
download link
* OR go to https://github.com/YosysHQ/oss-cad-suite-build/releases to download
the free OSS CAD Suite
* Follow the `Install Instructions on GitHub
<https://github.com/YosysHQ/oss-cad-suite-build#installation>`_
Make sure to get a Tabby CAD Suite Evaluation License for extensive
SystemVerilog Assertion (SVA) support, as well as industry-grade SystemVerilog
and VHDL parsers!
For more information about the difference between Tabby CAD Suite and the OSS
CAD Suite, please visit https://www.yosyshq.com/tabby-cad-datasheet.
Installing from source
**********************
Follow the instructions below to install sby and its dependencies. Yosys and sby
are non-optional. Boolector is recommended to install but not required. The
other packages are only required for some engine configurations.
Prerequisites
-------------
@ -18,137 +49,79 @@ Installing prerequisites (this command is for Ubuntu 16.04):
libboost-program-options-dev autoconf libgmp-dev \
cmake curl
Required components
-------------------
Yosys, Yosys-SMTBMC and ABC
---------------------------
^^^^^^^^^^^^^^^^^^^^^^^^^^^
https://yosyshq.net/yosys/
https://people.eecs.berkeley.edu/~alanmi/abc/
Next install Yosys, Yosys-SMTBMC and ABC (``yosys-abc``):
Note that this will install Yosys, Yosys-SMTBMC and ABC (as ``yosys-abc``):
.. code-block:: text
git clone https://github.com/YosysHQ/yosys.git yosys
git clone https://github.com/YosysHQ/yosys
cd yosys
make -j$(nproc)
sudo make install
SymbiYosys
----------
sby
^^^
https://github.com/YosysHQ/SymbiYosys
https://github.com/YosysHQ/sby
.. code-block:: text
git clone https://github.com/YosysHQ/SymbiYosys.git SymbiYosys
cd SymbiYosys
git clone https://github.com/YosysHQ/sby
cd sby
sudo make install
Yices 2
-------
http://yices.csl.sri.com/
.. code-block:: text
git clone https://github.com/SRI-CSL/yices2.git yices2
cd yices2
autoconf
./configure
make -j$(nproc)
sudo make install
Z3
--
https://github.com/Z3Prover/z3/wiki
.. code-block:: text
git clone https://github.com/Z3Prover/z3.git z3
cd z3
python scripts/mk_make.py
cd build
make -j$(nproc)
sudo make install
super_prove
-----------
https://github.com/sterin/super-prove-build
.. code-block:: text
sudo apt-get install cmake ninja-build g++ python-dev python-setuptools \
python-pip git
git clone --recursive https://github.com/sterin/super-prove-build
cd super-prove-build
mkdir build
cd build
cmake -DCMAKE_BUILD_TYPE=Release -G Ninja ..
ninja
ninja package
This creates a .tar.gz archive for the target system. Extract it to
``/usr/local/super_prove``
.. code-block:: text
sudo tar -C /usr/local -x super_prove-X-Y-Release.tar.gz
Then create a wrapper script ``/usr/local/bin/suprove`` with the following contents:
.. code-block:: text
#!/bin/bash
tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi
exec /usr/local/super_prove/bin/${tool}.sh "$@"
And make this wrapper script executable:
.. code-block:: text
sudo chmod +x /usr/local/bin/suprove
Avy
---
https://arieg.bitbucket.io/avy/
.. code-block:: text
git clone https://bitbucket.org/arieg/extavy.git
cd extavy
git submodule update --init
mkdir build; cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make -j$(nproc)
sudo cp avy/src/{avy,avybmc} /usr/local/bin/
Recommended components
----------------------
Boolector
---------
^^^^^^^^^
http://fmv.jku.at/boolector/
https://boolector.github.io
.. code-block:: text
git clone https://github.com/boolector/boolector
cd boolector
./contrib/setup-btor2tools.sh
./contrib/setup-lingeling.sh
./configure.sh
make -C build -j$(nproc)
sudo cp build/bin/{boolector,btor*} /usr/local/bin/
sudo cp deps/btor2tools/bin/btorsim /usr/local/bin/
git clone https://github.com/boolector/boolector
cd boolector
./contrib/setup-btor2tools.sh
./contrib/setup-lingeling.sh
./configure.sh
make -C build -j$(nproc)
sudo cp build/bin/{boolector,btor*} /usr/local/bin/
sudo cp deps/btor2tools/bin/btorsim /usr/local/bin/
To use the ``btor`` engine you will need to install btor2tools from
`commit c35cf1c <https://github.com/Boolector/btor2tools/commit/c35cf1c>`_ or
newer.
To use the ``btor`` engine you additionally need a newer version of btorsim than the boolector setup script builds:
Optional components
-------------------
Additional solver engines can be installed as per their instructions, links are
provided below.
.. code-block:: text
Z3
^^^
git clone https://github.com/boolector/btor2tools
cd btor2tools
./configure.sh
cmake . -DBUILD_SHARED_LIBS=OFF
make -j$(nproc)
sudo make install
https://github.com/Z3Prover/z3
Yices 2
^^^^^^^
http://yices.csl.sri.com/
https://github.com/SRI-CSL/yices2
super_prove
^^^^^^^^^^^
https://github.com/sterin/super-prove-build
Avy
^^^
https://arieg.bitbucket.io/avy/

2
docs/source/license.rst
View file

@ -1,5 +1,5 @@
SymbiYosys License
SymbiYosys license
==================
SymbiYosys (sby) itself is licensed under the ISC license:

BIN
docs/source/media/gtkwave_coverskip.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 13 KiB

BIN
docs/source/media/gtkwave_noskip.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 13 KiB

364
docs/source/quickstart.rst
View file

@ -1,119 +1,307 @@
Getting Started
Getting started
===============
The example files used in this chapter can be downloaded from `here
<https://github.com/YosysHQ/SymbiYosys/tree/master/docs/examples/quickstart>`_.
.. note::
First step: A simple BMC example
--------------------------------
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``.
Here is a simple example design with a safety property (assertion).
First In, First Out (FIFO) buffer
*********************************
.. literalinclude:: ../examples/quickstart/demo.sv
From `Wikipedia <https://en.wikipedia.org/wiki/FIFO_(computing_and_electronics)>`_,
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:
.. literalinclude:: ../examples/fifo/fifo.sv
:language: systemverilog
:start-at: address generator
:end-at: endmodule
The property in this example is true. We'd like to verify this using a bounded
model check (BMC) that is 100 cycles deep.
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.
SymbiYosys is controlled by ``.sby`` files. The following file can be used to
configure SymbiYosys to run a BMC for 100 cycles on the design:
Next, the register file:
.. literalinclude:: ../examples/quickstart/demo.sby
:language: text
.. literalinclude:: ../examples/fifo/fifo.sv
:language: systemverilog
:start-at: fifo storage
:end-before: end storage
:dedent:
Simply create a text file ``demo.sv`` with the example design and another text
file ``demo.sby`` with the SymbiYosys configuration. Then run::
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.
sby demo.sby
Verification properties
***********************
This will run a bounded model check for 100 cycles. The last few lines of the
output should look something like this:
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:
.. literalinclude:: ../examples/fifo/fifo.sv
:language: systemverilog
:start-at: a_oflow
:end-at: ;
:dedent:
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.
.. literalinclude:: ../examples/fifo/fifo.sv
:language: systemverilog
:start-at: a_counts
:end-at: ;
:dedent:
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.
.. literalinclude:: ../examples/fifo/fifo.sv
:language: systemverilog
:start-at: assign addr_diff
:end-at: ;
:dedent:
.. literalinclude:: ../examples/fifo/fifo.sv
:language: systemverilog
:start-at: a_count_diff
:end-at: ;
:dedent:
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.
.. literalinclude:: ../examples/fifo/fifo.sv
:language: systemverilog
:start-at: NO_FULL_SKIP
:end-at: endif
:lines: 1-5,9
The last few lines of output for the nofullskip task should be similar to the
following:
.. code-block:: text
SBY [demo] engine_0: ## 0 0:00:00 Checking asserts in step 96..
SBY [demo] engine_0: ## 0 0:00:00 Checking asserts in step 97..
SBY [demo] engine_0: ## 0 0:00:00 Checking asserts in step 98..
SBY [demo] engine_0: ## 0 0:00:00 Checking asserts in step 99..
SBY [demo] engine_0: ## 0 0:00:00 Status: PASSED
SBY [demo] engine_0: Status returned by engine: PASS
SBY [demo] engine_0: finished (returncode=0)
SBY [demo] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY [demo] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY [demo] summary: engine_0 (smtbmc) returned PASS
SBY [demo] DONE (PASS)
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']
This will also create a ``demo/`` directory tree with all relevant information,
such as a copy of the design source, various log files, and trace data in case
the proof fails.
Using the ``noskip.gtkw`` file provided, use the below command to examine the
error trace.
(Use ``sby -f demo.sby`` to re-run the proof. Without ``-f`` the command will
fail because the output directory ``demo/`` already exists.)
gtkwave fifo_nofullskip/engine_0/trace.vcd noskip.gtkw
Time for a simple exercise: Modify the design so that the property is false
and the offending state is reachable within 100 cycles. Re-run ``sby`` with
the modified design and see if the proof now fails. Inspect the counterexample
trace (``.vcd`` file) produced by ``sby``. (`GTKWave <http://gtkwave.sourceforge.net/>`_
is an open source VCD viewer that you can use.)
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.
Selecting the right engine
--------------------------
.. image:: media/gtkwave_noskip.png
The ``.sby`` file for a project selects one or more engines. (When multiple
engines are selected, all engines are executed in parallel and the result
returned by the first engine to finish is the result returned by SymbiYosys.)
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.
Each engine has its strengths and weaknesses. Therefore it is important to
select the right engine for each project. The documentation for the individual
engines can provide some guidance for engine selection. (Trial and error can
also be a useful method for evaluating engines.)
sby fifo.sby cover
Let's consider the following example:
Searching the file for ``w_underfill`` will reveal the below.
.. literalinclude:: ../examples/quickstart/memory.sv
.. code-block:: text
$ 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
.. image:: media/gtkwave_coverskip.png
.. 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.
.. code-block:: text
[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\ :sup:`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
*********************
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``.
.. literalinclude:: ../examples/fifo/fifo.sv
:language: systemverilog
:start-at: property write_skip
:end-at: w_underfill
:dedent:
This example is expected to fail verification (see the BUG comment).
The following ``.sby`` file can be used to show this:
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.
.. literalinclude:: ../examples/quickstart/memory.sby
:language: text
This project uses the ``smtbmc`` engine, which uses SMT solvers to perform the
proof. This engine uses the array-theories provided by those solvers to
efficiently model memories. Since this example uses large memories, the
``smtbmc`` engine is a good match.
(``smtbmc boolector`` selects Boolector as SMT solver, ``smtbmc z3`` selects
Z3, and ``smtbmc yices`` selects Yices 2. Yices 2 is the default solver when
no argument is used with ``smtbmc``.)
Exercise: The engine ``abc bmc3`` does not provide abstract memory models.
Therefore SymbiYosys has to synthesize the memories in the example to FFs
and address logic. How does the performance of this project change if
``abc bmc3`` is used as engine instead of ``smtbmc boolector``? How fast
can either engine verify the design when the bug has been fixed?
Beyond bounded model checks
---------------------------
Bounded model checks only prove that the safety properties hold for the first
*N* cycles (where *N* is the depth of the BMC). Sometimes this is insufficient
and we need to prove that the safety properties hold forever, not just the first
*N* cycles. Let us consider the following example:
.. literalinclude:: ../examples/quickstart/prove.sv
.. literalinclude:: ../examples/fifo/fifo.sv
:language: systemverilog
:start-at: reg past_nwen;
:end-before: end w_underfill
:dedent:
Proving this design in an unbounded manner can be achieved using the following
SymbiYosys configuration file:
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.
.. literalinclude:: ../examples/quickstart/prove.sby
:language: text
Note that ``mode`` is now set to ``prove`` instead of ``bmc``. The ``smtbmc``
engine in ``prove`` mode will perform a k-induction proof. Other engines can
use other methods, e.g. using ``abc pdr`` will prove the design using the IC3
algorithm.
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
<https://yosyshq.readthedocs.io/projects/ap109/en/latest/>`_.