riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
yosys/docs/source/using_yosys/more_scripting/interactive_investigation.rst

814 lines
34 KiB
ReStructuredText
Raw Blame History

Interactive design investigation
--------------------------------
.. todo:: interactive design opening text
.. role:: yoscrypt(code)
:language: yoscrypt
.. _interactive_show:
A look at the show command
~~~~~~~~~~~~~~~~~~~~~~~~~~
.. TODO:: merge into :doc:`/getting_started/scripting_intro` show section
This section explores the :cmd:ref:`show` command and explains the symbols used
in the circuit diagrams generated by it. The code used is included in the Yosys
code base under |code_examples/show|_.
.. |code_examples/show| replace:: :file:`docs/source/code_examples/show`
.. _code_examples/show: https://github.com/YosysHQ/yosys/tree/main/docs/source/code_examples/show
A simple circuit
^^^^^^^^^^^^^^^^
:ref:`example_v` below provides the Verilog code for a simple circuit which we
will use to demonstrate the usage of :cmd:ref:`show` in a simple setting.
.. literalinclude:: /code_examples/show/example.v
:language: Verilog
:caption: :file:`example.v`
:name: example_v
The Yosys synthesis script we will be running is included as
:numref:`example_ys`. Note that :cmd:ref:`show` is called with the ``-pause``
option, that halts execution of the Yosys script until the user presses the
Enter key. Using :yoscrypt:`show -pause` also allows the user to enter an
interactive shell to further investigate the circuit before continuing
synthesis.
.. literalinclude:: /code_examples/show/example_show.ys
:language: yoscrypt
:caption: :file:`example_show.ys`
:name: example_ys
This script, when executed, will show the design after each of the three
synthesis commands. We will now look at each of these diagrams and explain what
is shown.
.. note::
The images uses in this document are generated from the :file:`example.ys`
file, rather than :file:`example_show.ys`. :file:`example.ys` outputs the
schematics as :file:`.dot` files rather than displaying them directly. You
can view these images yourself by running :file:`yosys example.ys` and then
``xdot example_first.dot`` etc.
.. figure:: /_images/code_examples/show/example_first.*
:class: width-helper invert-helper
Output of the first :cmd:ref:`show` command in :numref:`example_ys`
The first output shows the design directly after being read by the Verilog
front-end. Input and output ports are displayed as octagonal shapes. Cells are
displayed as rectangles with inputs on the left and outputs on the right side.
The cell labels are two lines long: The first line contains a unique identifier
for the cell and the second line contains the cell type. Internal cell types are
prefixed with a dollar sign. For more details on the internal cell library, see
:doc:`/yosys_internals/formats/cell_library`.
Constants are shown as ellipses with the constant value as label. The syntax
``<bit_width>'<bits>`` is used for constants that are not 32-bit wide and/or
contain bits that are not 0 or 1 (i.e. ``x`` or ``z``). Ordinary 32-bit
constants are written using decimal numbers.
Single-bit signals are shown as thin arrows pointing from the driver to the
load. Signals that are multiple bits wide are shown as think arrows.
Finally *processes* are shown in boxes with round corners. Processes are Yosys'
internal representation of the decision-trees and synchronization events
modelled in a Verilog ``always``-block. The label reads ``PROC`` followed by a
unique identifier in the first line and contains the source code location of the
original ``always``-block in the second line. Note how the multiplexer from the
``?:``-expression is represented as a ``$mux`` cell but the multiplexer from the
``if``-statement is yet still hidden within the process.
The :cmd:ref:`proc` command transforms the process from the first diagram into a
multiplexer and a d-type flip-flop, which brings us to the second diagram:
.. figure:: /_images/code_examples/show/example_second.*
:class: width-helper invert-helper
Output of the second :cmd:ref:`show` command in :numref:`example_ys`
The Rhombus shape to the right is a dangling wire. (Wire nodes are only shown if
they are dangling or have "public" names, for example names assigned from the
Verilog input.) Also note that the design now contains two instances of a
``BUF``-node. These are artefacts left behind by the :cmd:ref:`proc` command. It
is quite usual to see such artefacts after calling commands that perform changes
in the design, as most commands only care about doing the transformation in the
least complicated way, not about cleaning up after them. The next call to
:cmd:ref:`clean` (or :cmd:ref:`opt`, which includes :cmd:ref:`clean` as one of
its operations) will clean up these artefacts. This operation is so common in
Yosys scripts that it can simply be abbreviated with the ``;;`` token, which
doubles as separator for commands. Unless one wants to specifically analyze this
artefacts left behind some operations, it is therefore recommended to always
call :cmd:ref:`clean` before calling :cmd:ref:`show`.
In this script we directly call :cmd:ref:`opt` as the next step, which finally
leads us to the third diagram:
.. figure:: /_images/code_examples/show/example_third.*
:class: width-helper invert-helper
:name: example_out
Output of the third :cmd:ref:`show` command in :ref:`example_ys`
Here we see that the :cmd:ref:`proc` command not only has removed the artifacts
left behind by :cmd:ref:`proc`, but also determined correctly that it can remove
the first ``$mux`` cell without changing the behavior of the circuit.
Break-out boxes for signal vectors
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The code listing below shows a simple circuit which uses a lot of spliced signal
accesses.
.. literalinclude:: /code_examples/show/splice.v
:caption: :file:`splice.v`
:name: splice_src
Notice how the output for this circuit from the :cmd:ref:`show` command
(:numref:`splice_dia`) appears quite complex. This is an unfortunate side effect
of the way Yosys handles signal vectors (aka. multi-bit wires or buses) as
native objects. While this provides great advantages when analyzing circuits
that operate on wide integers, it also introduces some additional complexity
when the individual bits of of a signal vector are accessed.
.. figure:: /_images/code_examples/show/splice.*
:class: width-helper invert-helper
:name: splice_dia
Output of ``yosys -p 'prep -top splice_demo; show' splice.v``
The key elements in understanding this circuit diagram are of course the boxes
with round corners and rows labeled ``<MSB_LEFT>:<LSB_LEFT> -
<MSB_RIGHT>:<LSB_RIGHT>``. Each of these boxes have one signal per row on one
side and a common signal for all rows on the other side. The ``<MSB>:<LSB>``
tuples specify which bits of the signals are broken out and connected. So the
top row of the box connecting the signals ``a`` and ``x`` indicates that the bit
0 (i.e. the range 0:0) from signal ``a`` is connected to bit 1 (i.e. the range
1:1) of signal ``x``.
Lines connecting such boxes together and lines connecting such boxes to cell
ports have a slightly different look to emphasise that they are not actual
signal wires but a necessity of the graphical representation. This distinction
seems like a technicality, until one wants to debug a problem related to the way
Yosys internally represents signal vectors, for example when writing custom
Yosys commands.
Gate level netlists
^^^^^^^^^^^^^^^^^^^
:numref:`first_pitfall` shows two common pitfalls when working with designs
mapped to a cell library:
.. figure:: /_images/code_examples/show/cmos_00.*
:class: width-helper invert-helper
:name: first_pitfall
A half-adder built from simple CMOS gates, demonstrating common pitfalls when
using :cmd:ref:`show`
.. literalinclude:: /code_examples/show/cmos.ys
:language: yoscrypt
:start-after: pitfall
:end-at: cmos_00
:name: pitfall_code
:caption: Generating :numref:`first_pitfall`
First, Yosys did not have access to the cell library when this diagram was
generated, resulting in all cell ports defaulting to being inputs. This is why
all ports are drawn on the left side the cells are awkwardly arranged in a large
column. Secondly the two-bit vector ``y`` requires breakout-boxes for its
individual bits, resulting in an unnecessary complex diagram.
.. figure:: /_images/code_examples/show/cmos_01.*
:class: width-helper invert-helper
:name: second_pitfall
Effects of :cmd:ref:`splitnets` command and of providing a cell library on
design in :numref:`first_pitfall`
.. literalinclude:: /code_examples/show/cmos.ys
:language: yoscrypt
:start-after: fixed
:end-at: cmos_01
:name: pitfall_avoided
:caption: Generating :numref:`second_pitfall`
For :numref:`second_pitfall`, Yosys has been given a description of the cell
library as Verilog file containing blackbox modules. There are two ways to load
cell descriptions into Yosys: First the Verilog file for the cell library can be
passed directly to the :cmd:ref:`show` command using the ``-lib <filename>``
option. Secondly it is possible to load cell libraries into the design with the
:yoscrypt:`read_verilog -lib <filename>` command. The second method has the
great advantage that the library only needs to be loaded once and can then be
used in all subsequent calls to the :cmd:ref:`show` command.
In addition to that, :numref:`second_pitfall` was generated after
:yoscrypt:`splitnet -ports` was run on the design. This command splits all
signal vectors into individual signal bits, which is often desirable when
looking at gate-level circuits. The ``-ports`` option is required to also split
module ports. Per default the command only operates on interior signals.
Miscellaneous notes
^^^^^^^^^^^^^^^^^^^
Per default the :cmd:ref:`show` command outputs a temporary dot file and
launches ``xdot`` to display it. The options ``-format``, ``-viewer`` and
``-prefix`` can be used to change format, viewer and filename prefix. Note that
the ``pdf`` and ``ps`` format are the only formats that support plotting
multiple modules in one run. The ``dot`` format can be used to output multiple
modules, however ``xdot`` will raise an error when trying to read them.
In densely connected circuits it is sometimes hard to keep track of the
individual signal wires. For these cases it can be useful to call
:cmd:ref:`show` with the ``-colors <integer>`` argument, which randomly assigns
colors to the nets. The integer (> 0) is used as seed value for the random color
assignments. Sometimes it is necessary it try some values to find an assignment
of colors that looks good.
The command :yoscrypt:`help show` prints a complete listing of all options
supported by the :cmd:ref:`show` command.
Navigating the design
~~~~~~~~~~~~~~~~~~~~~
Plotting circuit diagrams for entire modules in the design brings us only helps
in simple cases. For complex modules the generated circuit diagrams are just
stupidly big and are no help at all. In such cases one first has to select the
relevant portions of the circuit.
In addition to *what* to display one also needs to carefully decide *when* to
display it, with respect to the synthesis flow. In general it is a good idea to
troubleshoot a circuit in the earliest state in which a problem can be
reproduced. So if, for example, the internal state before calling the
:cmd:ref:`techmap` command already fails to verify, it is better to troubleshoot
the coarse-grain version of the circuit before :cmd:ref:`techmap` than the
gate-level circuit after :cmd:ref:`techmap`.
.. Note::
It is generally recommended to verify the internal state of a design by
writing it to a Verilog file using :yoscrypt:`write_verilog -noexpr` and
using the simulation models from :file:`simlib.v` and :file:`simcells.v` from
the Yosys data directory (as printed by ``yosys-config --datdir``).
Interactive navigation
^^^^^^^^^^^^^^^^^^^^^^
Once the right state within the synthesis flow for debugging the circuit has
been identified, it is recommended to simply add the :cmd:ref:`shell` command to
the matching place in the synthesis script. This command will stop the synthesis
at the specified moment and go to shell mode, where the user can interactively
enter commands.
For most cases, the shell will start with the whole design selected (i.e. when
the synthesis script does not already narrow the selection). The command
:cmd:ref:`ls` can now be used to create a list of all modules. The command
:cmd:ref:`cd` can be used to switch to one of the modules (type ``cd ..`` to
switch back). Now the :cmd:ref:`ls` command lists the objects within that
module. This is demonstrated below using :file:`example.v` from `A simple
circuit`_:
.. literalinclude:: /code_examples/show/example.out
:language: doscon
:start-at: yosys> ls
:end-before: yosys [example]> dump
:caption: Output of :cmd:ref:`ls` and :cmd:ref:`cd` after running :file:`yosys example.v`
:name: lscd
When a module is selected using the :cmd:ref:`cd` command, all commands (with a
few exceptions, such as the ``read_`` and ``write_`` commands) operate only on
the selected module. This can also be useful for synthesis scripts where
different synthesis strategies should be applied to different modules in the
design.
We can see that the cell names from :numref:`example_out` are just abbreviations
of the actual cell names, namely the part after the last dollar-sign. Most
auto-generated names (the ones starting with a dollar sign) are rather long and
contains some additional information on the origin of the named object. But in
most cases those names can simply be abbreviated using the last part.
Usually all interactive work is done with one module selected using the
:cmd:ref:`cd` command. But it is also possible to work from the design-context
(``cd ..``). In this case all object names must be prefixed with
``<module_name>/``. For example ``a*/b*`` would refer to all objects whose names
start with ``b`` from all modules whose names start with ``a``.
The :cmd:ref:`dump` command can be used to print all information about an
object. For example, calling :yoscrypt:`dump $2` after the :yoscrypt:`cd
example` above:
.. literalinclude:: /code_examples/show/example.out
:language: RTLIL
:start-after: yosys [example]> dump
:end-before: yosys [example]> cd
:dedent:
:caption: Output of :yoscrypt:`dump $2` after :numref:`lscd`
:name: dump2
This can for example be useful to determine the names of nets connected to
cells, as the net-names are usually suppressed in the circuit diagram if they
are auto-generated. Note that the output is in the RTLIL representation,
described in :doc:`/yosys_internals/formats/rtlil_rep`.
Interactive Design Investigation
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Yosys can also be used to investigate designs (or netlists created from other
tools).
- The selection mechanism, especially patterns such as ``%ci`` and ``%co``, can
be used to figure out how parts of the design are connected.
- Commands such as :cmd:ref:`submod`, :cmd:ref:`expose`, and :cmd:ref:`splice`
can be used to transform the design into an equivalent design that is easier
to analyse.
- Commands such as :cmd:ref:`eval` and :cmd:ref:`sat` can be used to investigate
the behavior of the circuit.
- :doc:`/cmd/show`.
- :doc:`/cmd/dump`.
- :doc:`/cmd/add` and :doc:`/cmd/delete` can be used to modify and reorganize a
design dynamically.
The code used is included in the Yosys code base under
|code_examples/scrambler|_.
.. |code_examples/scrambler| replace:: :file:`docs/source/code_examples/scrambler`
.. _code_examples/scrambler: https://github.com/YosysHQ/yosys/tree/main/docs/source/code_examples/scrambler
Changing design hierarchy
^^^^^^^^^^^^^^^^^^^^^^^^^
Commands such as :cmd:ref:`flatten` and :cmd:ref:`submod` can be used to change
the design hierarchy, i.e. flatten the hierarchy or moving parts of a module to
a submodule. This has applications in synthesis scripts as well as in reverse
engineering and analysis. An example using :cmd:ref:`submod` is shown below for
reorganizing a module in Yosys and checking the resulting circuit.
.. literalinclude:: /code_examples/scrambler/scrambler.v
:language: verilog
:caption: :file:`scrambler.v`
.. literalinclude:: /code_examples/scrambler/scrambler.ys
:language: yoscrypt
:caption: :file:`scrambler.ys`
:end-before: cd ..
.. figure:: /_images/code_examples/scrambler/scrambler_p01.*
:class: width-helper invert-helper
.. figure:: /_images/code_examples/scrambler/scrambler_p02.*
:class: width-helper invert-helper
Analyzing the resulting circuit with :doc:`/cmd/eval`:
.. todo:: replace inline code
.. code:: text
> cd xorshift32
> rename n2 in
> rename n1 out
> eval -set in 1 -show out
Eval result: \out = 270369.
> eval -set in 270369 -show out
Eval result: \out = 67634689.
> sat -set out 632435482
Signal Name Dec Hex Bin
-------------------- ---------- ---------- -------------------------------------
\in 745495504 2c6f5bd0 00101100011011110101101111010000
\out 632435482 25b2331a 00100101101100100011001100011010
Behavioral changes
^^^^^^^^^^^^^^^^^^
Commands such as :cmd:ref:`techmap` can be used to make behavioral changes to
the design, for example changing asynchronous resets to synchronous resets. This
has applications in design space exploration (evaluation of various
architectures for one circuit).
The following techmap map file replaces all positive-edge async reset flip-flops
with positive-edge sync reset flip-flops. The code is taken from the example
Yosys script for ASIC synthesis of the Amber ARMv2 CPU.
.. todo:: replace inline code
.. code:: verilog
(* techmap_celltype = "$adff" *)
module adff2dff (CLK, ARST, D, Q);
parameter WIDTH = 1;
parameter CLK_POLARITY = 1;
parameter ARST_POLARITY = 1;
parameter ARST_VALUE = 0;
input CLK, ARST;
input [WIDTH-1:0] D;
output reg [WIDTH-1:0] Q;
wire [1023:0] _TECHMAP_DO_ = "proc";
wire _TECHMAP_FAIL_ = !CLK_POLARITY || !ARST_POLARITY;
always @(posedge CLK)
if (ARST)
Q <= ARST_VALUE;
else
Q <= D;
endmodule
For more on the :cmd:ref:`techmap` command, see the page on
:doc:`/yosys_internals/techmap`.
Advanced investigation techniques
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When working with very large modules, it is often not enough to just select the
interesting part of the module. Instead it can be useful to extract the
interesting part of the circuit into a separate module. This can for example be
useful if one wants to run a series of synthesis commands on the critical part
of the module and wants to carefully read all the debug output created by the
commands in order to spot a problem. This kind of troubleshooting is much easier
if the circuit under investigation is encapsulated in a separate module.
Recall the ``memdemo`` design from :ref:`advanced_logic_cones`:
.. figure:: /_images/code_examples/selections/memdemo_00.*
:class: width-helper invert-helper
``memdemo``
Because this produces a rather large circuit, it can be useful to split it into
smaller parts for viewing and working with. :numref:`submod` does exactly that,
utilising the :cmd:ref:`submod` command to split the circuit into three
sections: ``outstage``, ``selstage``, and ``scramble``.
.. literalinclude:: /code_examples/selections/submod.ys
:language: yoscrypt
:caption: Using :cmd:ref:`submod` to break up the circuit from :file:`memdemo.v`
:start-after: cd memdemo
:end-before: cd ..
:name: submod
The ``-name`` option is used to specify the name of the new module and also the
name of the new cell in the current module. The resulting circuits are shown
below.
.. figure:: /_images/code_examples/selections/submod_02.*
:class: width-helper invert-helper
``outstage``
.. figure:: /_images/code_examples/selections/submod_03.*
:class: width-helper invert-helper
:name: selstage
``selstage``
.. figure:: /_images/code_examples/selections/submod_01.*
:class: width-helper invert-helper
``scramble``
Evaluation of combinatorial circuits
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The :cmd:ref:`eval` command can be used to evaluate combinatorial circuits. As
an example, we will use the ``selstage`` subnet of ``memdemo`` which we found
above and is shown in :numref:`selstage`.
.. todo:: replace inline code
::
yosys [selstage]> eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1
1. Executing EVAL pass (evaluate the circuit given an input).
Full command line: eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1
Eval result: \n2 = 2'10.
Eval result: \n1 = 2'10.
So the ``-set`` option is used to set input values and the ``-show`` option is
used to specify the nets to evaluate. If no ``-show`` option is specified, all
selected output ports are used per default.
If a necessary input value is not given, an error is produced. The option
``-set-undef`` can be used to instead set all unspecified input nets to undef
(``x``).
The ``-table`` option can be used to create a truth table. For example:
::
yosys [selstage]> eval -set-undef -set d[3:1] 0 -table s1,d[0]
10. Executing EVAL pass (evaluate the circuit given an input).
Full command line: eval -set-undef -set d[3:1] 0 -table s1,d[0]
\s1 \d [0] | \n1 \n2
---- ------ | ---- ----
2'00 1'0 | 2'00 2'00
2'00 1'1 | 2'xx 2'00
2'01 1'0 | 2'00 2'00
2'01 1'1 | 2'xx 2'01
2'10 1'0 | 2'00 2'00
2'10 1'1 | 2'xx 2'10
2'11 1'0 | 2'00 2'00
2'11 1'1 | 2'xx 2'11
Assumed undef (x) value for the following signals: \s2
Note that the :cmd:ref:`eval` command (as well as the :cmd:ref:`sat` command
discussed in the next sections) does only operate on flattened modules. It can
not analyze signals that are passed through design hierarchy levels. So the
:cmd:ref:`flatten` command must be used on modules that instantiate other
modules before these commands can be applied.
Solving combinatorial SAT problems
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Often the opposite of the :cmd:ref:`eval` command is needed, i.e. the circuits
output is given and we want to find the matching input signals. For small
circuits with only a few input bits this can be accomplished by trying all
possible input combinations, as it is done by the ``eval -table`` command. For
larger circuits however, Yosys provides the :cmd:ref:`sat` command that uses a
`SAT`_ solver, `MiniSAT`_, to solve this kind of problems.
.. _SAT: http://en.wikipedia.org/wiki/Circuit_satisfiability
.. _MiniSAT: http://minisat.se/
.. note::
While it is possible to perform model checking directly in Yosys, it
is highly recommended to use SBY or EQY for formal hardware verification.
The :cmd:ref:`sat` command works very similar to the :cmd:ref:`eval` command.
The main difference is that it is now also possible to set output values and
find the corresponding input values. For Example:
.. todo:: replace inline code
::
yosys [selstage]> sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001
11. Executing SAT pass (solving SAT problems in the circuit).
Full command line: sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001
Setting up SAT problem:
Import set-constraint: \s1 = \s2
Import set-constraint: { \n2 \n1 } = 4'1001
Final constraint equation: { \n2 \n1 \s1 } = { 4'1001 \s2 }
Imported 3 cells to SAT database.
Import show expression: { \s1 \s2 \d }
Solving problem with 81 variables and 207 clauses..
SAT solving finished - model found:
Signal Name Dec Hex Bin
-------------------- ---------- ---------- ---------------
\d 9 9 1001
\s1 0 0 00
\s2 0 0 00
Note that the :cmd:ref:`sat` command supports signal names in both arguments to
the ``-set`` option. In the above example we used ``-set s1 s2`` to constraint
``s1`` and ``s2`` to be equal. When more complex constraints are needed, a
wrapper circuit must be constructed that checks the constraints and signals if
the constraint was met using an extra output port, which then can be forced to a
value using the ``-set`` option. (Such a circuit that contains the circuit under
test plus additional constraint checking circuitry is called a ``miter``
circuit.)
.. literalinclude:: /code_examples/primetest.v
:language: verilog
:caption: :file:`primetest.v`, a simple miter circuit for testing if a number is
prime. But it has a problem.
:name: primetest
:numref:`primetest` shows a miter circuit that is supposed to be used as a prime
number test. If ``ok`` is 1 for all input values ``a`` and ``b`` for a given
``p``, then ``p`` is prime, or at least that is the idea.
.. todo:: replace inline code
.. code-block::
:caption: Experiments with the miter circuit from :file:`primetest.v`.
:name: prime_shell
yosys [primetest]> sat -prove ok 1 -set p 31
1. Executing SAT pass (solving SAT problems in the circuit).
Full command line: sat -prove ok 1 -set p 31
Setting up SAT problem:
Import set-constraint: \p = 16'0000000000011111
Final constraint equation: \p = 16'0000000000011111
Imported 6 cells to SAT database.
Import proof-constraint: \ok = 1'1
Final proof equation: \ok = 1'1
Solving problem with 2790 variables and 8241 clauses..
SAT proof finished - model found: FAIL!
______ ___ ___ _ _ _ _
(_____ \ / __) / __) (_) | | | |
_____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |
| ____/ ___) _ \ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|
| | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_
|_| |_| \___/ \___/ |_| |_| \_____|_|\_)_____)\____|_|
Signal Name Dec Hex Bin
-------------------- ---------- ---------- ---------------------
\a 15029 3ab5 0011101010110101
\b 4099 1003 0001000000000011
\ok 0 0 0
\p 31 1f 0000000000011111
The Yosys shell session shown in :numref:`prime_shell` demonstrates that SAT
solvers can even find the unexpected solutions to a problem: Using integer
overflow there actually is a way of "factorizing" 31. The clean solution would
of course be to perform the test in 32 bits, for example by replacing ``p !=
a*b`` in the miter with ``p != {16'd0,a}b``, or by using a temporary variable
for the 32 bit product ``a*b``. But as 31 fits well into 8 bits (and as the
purpose of this document is to show off Yosys features) we can also simply force
the upper 8 bits of ``a`` and ``b`` to zero for the :cmd:ref:`sat` call, as is
done below.
.. todo:: replace inline code
.. code-block::
:caption: Miter circuit from :file:`primetest.v`, with the upper 8 bits of ``a``
and ``b`` constrained to prevent overflow.
:name: prime_fixed
yosys [primetest]> sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0
1. Executing SAT pass (solving SAT problems in the circuit).
Full command line: sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0
Setting up SAT problem:
Import set-constraint: \p = 16'0000000000011111
Import set-constraint: { \a [15:8] \b [15:8] } = 16'0000000000000000
Final constraint equation: { \a [15:8] \b [15:8] \p } = { 16'0000000000000000 16'0000000000011111 }
Imported 6 cells to SAT database.
Import proof-constraint: \ok = 1'1
Final proof equation: \ok = 1'1
Solving problem with 2790 variables and 8257 clauses..
SAT proof finished - no model found: SUCCESS!
/$$$$$$ /$$$$$$$$ /$$$$$$$
/$$__ $$ | $$_____/ | $$__ $$
| $$ \ $$ | $$ | $$ \ $$
| $$ | $$ | $$$$$ | $$ | $$
| $$ | $$ | $$__/ | $$ | $$
| $$/$$ $$ | $$ | $$ | $$
| $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$
\____ $$$|__/|________/|__/|_______/|__/
\__/
The ``-prove`` option used in :numref:`prime_fixed` works similar to ``-set``,
but tries to find a case in which the two arguments are not equal. If such a
case is not found, the property is proven to hold for all inputs that satisfy
the other constraints.
It might be worth noting, that SAT solvers are not particularly efficient at
factorizing large numbers. But if a small factorization problem occurs as part
of a larger circuit problem, the Yosys SAT solver is perfectly capable of
solving it.
Solving sequential SAT problems
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The SAT solver functionality in Yosys can not only be used to solve
combinatorial problems, but can also solve sequential problems. Let's consider
the ``memdemo`` design from :ref:`advanced_logic_cones` again, and suppose we
want to know which sequence of input values for ``d`` will cause the output y to
produce the sequence 1, 2, 3 from any initial state. Let's use the following
command:
.. todo:: replace inline code?
.. code-block:: yoscrypt
sat -seq 6 -show y -show d -set-init-undef \
-max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3
The ``-seq 6`` option instructs the :cmd:ref:`sat` command to solve a sequential
problem in 6 time steps. (Experiments with lower number of steps have show that
at least 3 cycles are necessary to bring the circuit in a state from which the
sequence 1, 2, 3 can be produced.)
The ``-set-init-undef`` option tells the :cmd:ref:`sat` command to initialize
all registers to the undef (``x``) state. The way the ``x`` state is treated in
Verilog will ensure that the solution will work for any initial state.
The ``-max_undef`` option instructs the :cmd:ref:`sat` command to find a
solution with a maximum number of undefs. This way we can see clearly which
inputs bits are relevant to the solution.
Finally the three ``-set-at`` options add constraints for the ``y`` signal to
play the 1, 2, 3 sequence, starting with time step 4.
This produces the following output:
.. todo:: replace inline code
.. code-block::
:caption: Solving a sequential SAT problem in the ``memdemo`` module.
:name: memdemo_sat
yosys [memdemo]> sat -seq 6 -show y -show d -set-init-undef \
-max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3
1. Executing SAT pass (solving SAT problems in the circuit).
Full command line: sat -seq 6 -show y -show d -set-init-undef
-max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3
Setting up time step 1:
Final constraint equation: { } = { }
Imported 29 cells to SAT database.
Setting up time step 2:
Final constraint equation: { } = { }
Imported 29 cells to SAT database.
Setting up time step 3:
Final constraint equation: { } = { }
Imported 29 cells to SAT database.
Setting up time step 4:
Import set-constraint for timestep: \y = 4'0001
Final constraint equation: \y = 4'0001
Imported 29 cells to SAT database.
Setting up time step 5:
Import set-constraint for timestep: \y = 4'0010
Final constraint equation: \y = 4'0010
Imported 29 cells to SAT database.
Setting up time step 6:
Import set-constraint for timestep: \y = 4'0011
Final constraint equation: \y = 4'0011
Imported 29 cells to SAT database.
Setting up initial state:
Final constraint equation: { \y \s2 \s1 \mem[3] \mem[2] \mem[1]
\mem[0] } = 24'xxxxxxxxxxxxxxxxxxxxxxxx
Import show expression: \y
Import show expression: \d
Solving problem with 10322 variables and 27881 clauses..
SAT model found. maximizing number of undefs.
SAT solving finished - model found:
Time Signal Name Dec Hex Bin
---- -------------------- ---------- ---------- ---------------
init \mem[0] -- -- xxxx
init \mem[1] -- -- xxxx
init \mem[2] -- -- xxxx
init \mem[3] -- -- xxxx
init \s1 -- -- xx
init \s2 -- -- xx
init \y -- -- xxxx
---- -------------------- ---------- ---------- ---------------
1 \d 0 0 0000
1 \y -- -- xxxx
---- -------------------- ---------- ---------- ---------------
2 \d 1 1 0001
2 \y -- -- xxxx
---- -------------------- ---------- ---------- ---------------
3 \d 2 2 0010
3 \y 0 0 0000
---- -------------------- ---------- ---------- ---------------
4 \d 3 3 0011
4 \y 1 1 0001
---- -------------------- ---------- ---------- ---------------
5 \d -- -- 001x
5 \y 2 2 0010
---- -------------------- ---------- ---------- ---------------
6 \d -- -- xxxx
6 \y 3 3 0011
It is not surprising that the solution sets ``d = 0`` in the first step, as this
is the only way of setting the ``s1`` and ``s2`` registers to a known value. The
input values for the other steps are a bit harder to work out manually, but the
SAT solver finds the correct solution in an instant.
There is much more to write about the :cmd:ref:`sat` command. For example, there
is a set of options that can be used to performs sequential proofs using
temporal induction :cite:p:`een2003temporal`. The command ``help sat`` can be
used to print a list of all options with short descriptions of their functions.
Reference in New Issue View Git Blame Copy Permalink