mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-05 22:14:08 +00:00
Moving newstart to replace quickstart
This commit is contained in:
KrystalDelusion
parent
df2610d598
commit
82a6edf295
|
|
@ -15,7 +15,7 @@ formal tasks:
|
|||
:maxdepth: 3
|
||||
|
||||
install.rst
|
||||
newstart.rst
|
||||
quickstart.rst
|
||||
reference.rst
|
||||
autotune.rst
|
||||
verilog.rst
|
||||
|
|
|
|||
|
|
@ -1,307 +0,0 @@
|
|||
|
||||
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
|
||||
*********************************
|
||||
|
||||
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
|
||||
|
||||
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:
|
||||
|
||||
.. literalinclude:: ../examples/fifo/fifo.sv
|
||||
:language: systemverilog
|
||||
:start-at: fifo storage
|
||||
:end-before: end storage
|
||||
:dedent:
|
||||
|
||||
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:
|
||||
|
||||
.. 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 [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.
|
||||
|
||||
.. image:: media/gtkwave_noskip.png
|
||||
|
||||
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.
|
||||
|
||||
.. 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 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/fifo/fifo.sv
|
||||
:language: systemverilog
|
||||
:start-at: reg past_nwen;
|
||||
:end-before: end w_underfill
|
||||
:dedent:
|
||||
|
||||
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
|
||||
<https://yosyshq.readthedocs.io/projects/ap109/en/latest/>`_.
|
||||
|
|
@ -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/>`_.
|
||||
|
|
|
|||
Loading…
Reference in a new issue