diff options
Diffstat (limited to 'docs/source/appendix/APPNOTE_011_Design_Investigation.rst')
| -rw-r--r-- | docs/source/appendix/APPNOTE_011_Design_Investigation.rst | 965 |
1 files changed, 965 insertions, 0 deletions
diff --git a/docs/source/appendix/APPNOTE_011_Design_Investigation.rst b/docs/source/appendix/APPNOTE_011_Design_Investigation.rst new file mode 100644 index 000000000..004d3cb66 --- /dev/null +++ b/docs/source/appendix/APPNOTE_011_Design_Investigation.rst @@ -0,0 +1,965 @@ +========================================== +011: Interactive design investigation page +========================================== + +Installation and prerequisites +============================== + +This Application Note is based on the `Yosys GIT`_ `Rev. 2b90ba1`_ from +2013-12-08. The README file covers how to install Yosys. The ``show`` command +requires a working installation of `GraphViz`_ and `xdot` for generating the +actual circuit diagrams. + +.. _Yosys GIT: https://github.com/YosysHQ/yosys + +.. _Rev. 2b90ba1: https://github.com/YosysHQ/yosys/tree/2b90ba1 + +.. _GraphViz: http://www.graphviz.org/ + +.. _xdot: https://github.com/jrfonseca/xdot.py + +Overview +======== + +This application note is structured as follows: + +:ref:`intro_show` introduces the ``show`` command and explains the symbols used +in the circuit diagrams generated by it. + +:ref:`navigate` introduces additional commands used to navigate in the design, +select portions of the design, and print additional information on the elements +in the design that are not contained in the circuit diagrams. + +:ref:`poke` introduces commands to evaluate the design and solve SAT problems +within the design. + +:ref:`conclusion` concludes the document and summarizes the key points. + +.. _intro_show: + +Introduction to the show command +================================ + +.. code-block:: console + :caption: Yosys script with ``show`` commands and example design + :name: example_src + + $ cat example.ys + read_verilog example.v + show -pause + proc + show -pause + opt + show -pause + + $ cat example.v + module example(input clk, a, b, c, + output reg [1:0] y); + always @(posedge clk) + if (c) + y <= c ? a + b : 2'd0; + endmodule + +.. figure:: ../../images/011/example_out.* + :class: width-helper + :name: example_out + + Output of the three ``show`` commands from :numref:`example_src` + +The ``show`` command generates a circuit diagram for the design in its current +state. Various options can be used to change the appearance of the circuit +diagram, set the name and format for the output file, and so forth. When called +without any special options, it saves the circuit diagram in a temporary file +and launches ``xdot`` to display the diagram. Subsequent calls to show re-use the +``xdot`` instance (if still running). + +A simple circuit +---------------- + +:numref:`example_src` shows a simple synthesis script and a Verilog file that +demonstrate the usage of show in a simple setting. Note that ``show`` is called with +the ``-pause`` option, that halts execution of the Yosys script until the user +presses the Enter key. The ``show -pause`` command also allows the user to enter +an interactive shell to further investigate the circuit before continuing +synthesis. + +So this script, when executed, will show the design after each of the three +synthesis commands. The generated circuit diagrams are shown in +:numref:`example_out`. + +The first diagram (from top to bottom) 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. The Yosys manual contains a +chapter on the internal cell library used in Yosys. + +Constants are shown as ellipses with the constant value as label. The syntax +``<bit_width>'<bits>`` is used for 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 2nd 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 ``proc`` command transforms the process from the first diagram into a +multiplexer and a d-type flip-flip, which brings us to the 2nd diagram. + +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. This are artefacts left behind by the ``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 +``clean`` (or ``opt``, which includes ``clean`` as one of its operations) will +clean up this 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 ``clean`` before +calling ``show``. + +In this script we directly call ``opt`` as next step, which finally leads us to +the 3rd diagram in :numref:`example_out`. Here we see that the ``opt`` command +not only has removed the artifacts left behind by ``proc``, but also determined +correctly that it can remove the first ``$mux`` cell without changing the +behavior of the circuit. + +.. figure:: ../../images/011/splice.* + :class: width-helper + :name: splice_dia + + Output of ``yosys -p 'proc; opt; show' splice.v`` + +.. literalinclude:: ../../../manual/APPNOTE_011_Design_Investigation/splice.v + :caption: ``splice.v`` + :name: splice_src + +.. figure:: ../../images/011/splitnets_libfile.* + :class: width-helper + :name: splitnets_libfile + + Effects of ``splitnets`` command and of providing a cell library. (The + circuit is a half-adder built from simple CMOS gates.) + +Break-out boxes for signal vectors +---------------------------------- + +As has been indicated by the last example, Yosys is can manage signal vectors +(aka. multi-bit wires or buses) as native objects. This provides great +advantages when analyzing circuits that operate on wide integers. But it also +introduces some additional complexity when the individual bits of of a signal +vector are accessed. The example ``show`` in :numref:`splice_src` demonstrates +how such circuits are visualized by the ``show`` command. + +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 this boxes has 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 +------------------- + +Finally :numref:`splitnets_libfile` shows two common pitfalls when working with +designs mapped to a cell library. The top figure has two problems: 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. + +For the 2nd diagram 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 ``show`` command using the ``-lib <filename>`` option. +Secondly it is possible to load cell libraries into the design with the +``read_verilog -lib <filename>`` command. The 2nd 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 ``show`` command. + +In addition to that, the 2nd diagram was generated after ``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 ``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. + +In densely connected circuits it is sometimes hard to keep track of the +individual signal wires. For this cases it can be useful to call ``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 ``help show`` prints a complete listing of all options supported by +the ``show`` command. + +.. _navigate: + +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 ``techmap`` command already fails to verify, it is better to +troubleshoot the coarse-grain version of the circuit before ``techmap`` than +the gate-level circuit after ``techmap``. + +.. Note:: It is generally recommended to verify the internal state of a + design by writing it to a Verilog file using ``write_verilog -noexpr`` + and using the simulation models from ``simlib.v`` and ``simcells.v`` + from the Yosys data directory (as printed by ``yosys-config --datdir``). + +Interactive navigation +---------------------- + +.. code-block:: none + :caption: Demonstration of ``ls`` and ``cd`` using ``example.v`` from :numref:`example_src` + :name: lscd + + yosys> ls + + 1 modules: + example + + yosys> cd example + + yosys [example]> ls + + 7 wires: + $0\y[1:0] + $add$example.v:5$2_Y + a + b + c + clk + y + + 3 cells: + $add$example.v:5$2 + $procdff$7 + $procmux$5 + +.. code-block:: RTLIL + :caption: Output of ``dump \$2`` using the design from :numref:`example_src` + and :numref:`example_out` + :name: dump2 + + attribute \src "example.v:5" + cell $add $add$example.v:5$2 + parameter \A_SIGNED 0 + parameter \A_WIDTH 1 + parameter \B_SIGNED 0 + parameter \B_WIDTH 1 + parameter \Y_WIDTH 2 + connect \A \a + connect \B \b + connect \Y $add$example.v:5$2_Y + end + +Once the right state within the synthesis flow for debugging the circuit has +been identified, it is recommended to simply add the ``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 ``ls`` +can now be used to create a list of all modules. The command ``cd`` can be used +to switch to one of the modules (type ``cd ..`` to switch back). Now the `ls` +command lists the objects within that module. :numref:`lscd` demonstrates this +using the design from :numref:`example_src`. + +There is a thing to note in :numref:`lscd`: 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 ``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 ``dump`` command can be used to print all information about an object. For +example ``dump $2`` will print :numref:`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. + +For the remainder of this document we will assume that the commands are +run from module-context and not design-context. + +Working with selections +----------------------- + +.. figure:: ../../images/011/example_03.* + :class: width-helper + :name: seladd + + Output of ``show`` after ``select $2`` or ``select t:$add`` (see also + :numref:`example_out`) + +When a module is selected using the ``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. + +But for most interactive work we want to further narrow the set of +selected objects. This can be done using the ``select`` command. + +For example, if the command ``select $2`` is executed, a subsequent ``show`` +command will yield the diagram shown in :numref:`seladd`. Note that the nets are +now displayed in ellipses. This indicates that they are not selected, but only +shown because the diagram contains a cell that is connected to the net. This of +course makes no difference for the circuit that is shown, but it can be a useful +information when manipulating selections. + +Objects can not only be selected by their name but also by other properties. For +example ``select t:$add`` will select all cells of type ``$add``. In this case +this is also yields the diagram shown in :numref:`seladd`. + +.. literalinclude:: ../../../manual/APPNOTE_011_Design_Investigation/foobaraddsub.v + :caption: Test module for operations on selections + :name: foobaraddsub + :language: verilog + +The output of ``help select`` contains a complete syntax reference for +matching different properties. + +Many commands can operate on explicit selections. For example the command ``dump +t:$add`` will print information on all ``$add`` cells in the active module. +Whenever a command has ``[selection]`` as last argument in its usage help, this +means that it will use the engine behind the ``select`` command to evaluate +additional arguments and use the resulting selection instead of the selection +created by the last ``select`` command. + +Normally the ``select`` command overwrites a previous selection. The commands +``select -add`` and ``select -del`` can be used to add or remove objects from +the current selection. + +The command ``select -clear`` can be used to reset the selection to the default, +which is a complete selection of everything in the current module. + +Operations on selections +------------------------ + +.. literalinclude:: ../../../manual/APPNOTE_011_Design_Investigation/sumprod.v + :caption: Another test module for operations on selections + :name: sumprod + :language: verilog + +.. figure:: ../../images/011/sumprod_00.* + :class: width-helper + :name: sumprod_00 + + Output of ``show a:sumstuff`` on :numref:`sumprod` + +The ``select`` command is actually much more powerful than it might seem on the +first glimpse. When it is called with multiple arguments, each argument is +evaluated and pushed separately on a stack. After all arguments have been +processed it simply creates the union of all elements on the stack. So the +following command will select all ``$add`` cells and all objects with the +``foo`` attribute set: + +.. code-block:: yoscrypt + + select t:$add a:foo + +(Try this with the design shown in :numref:`foobaraddsub`. Use the ``select +-list`` command to list the current selection.) + +In many cases simply adding more and more stuff to the selection is an +ineffective way of selecting the interesting part of the design. Special +arguments can be used to combine the elements on the stack. For example +the ``%i`` arguments pops the last two elements from the stack, intersects +them, and pushes the result back on the stack. So the following command +will select all ``$add ``cells that have the ``foo`` attribute set: + +.. code-block:: yoscrypt + + select t:$add a:foo %i + +The listing in :numref:`sumprod` uses the Yosys non-standard ``{... \*}`` syntax +to set the attribute ``sumstuff`` on all cells generated by the first assign +statement. (This works on arbitrary large blocks of Verilog code an can be used +to mark portions of code for analysis.) + +Selecting ``a:sumstuff`` in this module will yield the circuit diagram shown in +:numref:`sumprod_00`. As only the cells themselves are selected, but not the +temporary wire ``$1_Y``, the two adders are shown as two disjunct parts. This +can be very useful for global signals like clock and reset signals: just +unselect them using a command such as ``select -del clk rst`` and each cell +using them will get its own net label. + +In this case however we would like to see the cells connected properly. This can +be achieved using the ``%x`` action, that broadens the selection, i.e. for each +selected wire it selects all cells connected to the wire and vice versa. So +``show a:sumstuff %x`` yields the diagram shown in :numref:`sumprod_01`. + +.. figure:: ../../images/011/sumprod_01.* + :class: width-helper + :name: sumprod_01 + + Output of ``show a:sumstuff %x`` on :numref:`sumprod` + +Selecting logic cones +--------------------- + +:numref:`sumprod_01` shows what is called the ``input cone`` of ``sum``, i.e. +all cells and signals that are used to generate the signal ``sum``. The ``%ci`` +action can be used to select the input cones of all object in the top selection +in the stack maintained by the ``select`` command. + +As the ``%x`` action, this commands broadens the selection by one "step". +But this time the operation only works against the direction of data +flow. That means, wires only select cells via output ports and cells +only select wires via input ports. + +:numref:`select_prod` show the sequence of diagrams generated by the following +commands: + +.. code-block:: yoscrypt + + show prod + show prod %ci + show prod %ci %ci + show prod %ci %ci %ci + +When selecting many levels of logic, repeating ``%ci`` over and over again can +be a bit dull. So there is a shortcut for that: the number of iterations can be +appended to the action. So for example the action ``%ci3`` is identical to +performing the ``%ci`` action three times. + +The action ``%ci\*`` performs the ``%ci`` action over and over again until it +has no effect anymore. + +.. figure:: ../../images/011/select_prod.* + :class: width-helper + :name: select_prod + + Objects selected by ``select prod \%ci...`` + +In most cases there are certain cell types and/or ports that should not be +considered for the ``%ci`` action, or we only want to follow certain cell types +and/or ports. This can be achieved using additional patterns that can be +appended to the ``%ci`` action. + +Lets consider the design from :numref:`memdemo_src`. It serves no purpose other +than being a non-trivial circuit for demonstrating some of the advanced Yosys +features. We synthesize the circuit using ``proc; opt; memory; opt`` and change +to the ``memdemo`` module with ``cd memdemo``. If we type ``show`` now we see +the diagram shown in :numref:`memdemo_00`. + +.. literalinclude:: ../../../manual/APPNOTE_011_Design_Investigation/memdemo.v + :caption: Demo circuit for demonstrating some advanced Yosys features + :name: memdemo_src + :language: verilog + +.. figure:: ../../images/011/memdemo_00.* + :class: width-helper + :name: memdemo_00 + + Complete circuit diagram for the design shown in :numref:`memdemo_src` + +But maybe we are only interested in the tree of multiplexers that select the +output value. In order to get there, we would start by just showing the output +signal and its immediate predecessors: + +.. code-block:: yoscrypt + + show y %ci2 + +From this we would learn that ``y`` is driven by a ``$dff cell``, that ``y`` is +connected to the output port ``Q``, that the ``clk`` signal goes into the +``CLK`` input port of the cell, and that the data comes from a auto-generated +wire into the input ``D`` of the flip-flop cell. + +As we are not interested in the clock signal we add an additional pattern to the +``%ci`` action, that tells it to only follow ports ``Q`` and ``D`` of ``$dff`` +cells: + +.. code-block:: yoscrypt + + show y %ci2:+$dff[Q,D] + +To add a pattern we add a colon followed by the pattern to the ``%ci`` action. +The pattern it self starts with ``-`` or ``+``, indicating if it is an include +or exclude pattern, followed by an optional comma separated list of cell types, +followed by an optional comma separated list of port names in square brackets. + +Since we know that the only cell considered in this case is a ``$dff`` cell, +we could as well only specify the port names: + +.. code-block:: yoscrypt + + show y %ci2:+[Q,D] + +Or we could decide to tell the ``%ci`` action to not follow the ``CLK`` input: + +.. code-block:: yoscrypt + + show y %ci2:-[CLK] + +.. figure:: ../../images/011/memdemo_01.* + :class: width-helper + :name: memdemo_01 + + Output of ``show y \%ci2:+\$dff[Q,D] \%ci*:-\$mux[S]:-\$dff`` + +Next we would investigate the next logic level by adding another ``%ci2`` to +the command: + +.. code-block:: yoscrypt + + show y %ci2:-[CLK] %ci2 + +From this we would learn that the next cell is a ``$mux`` cell and we would +add additional pattern to narrow the selection on the path we are +interested. In the end we would end up with a command such as + +.. code-block:: yoscrypt + + show y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff + +in which the first ``%ci`` jumps over the initial d-type flip-flop and the 2nd +action selects the entire input cone without going over multiplexer select +inputs and flip-flop cells. The diagram produces by this command is shown in +:numref:`memdemo_01`. + +Similar to ``%ci`` exists an action ``%co`` to select output cones that accepts +the same syntax for pattern and repetition. The ``%x`` action mentioned +previously also accepts this advanced syntax. + +This actions for traversing the circuit graph, combined with the actions for +boolean operations such as intersection (``%i``) and difference (``%d``) are +powerful tools for extracting the relevant portions of the circuit under +investigation. + +See ``help select`` for a complete list of actions available in selections. + +Storing and recalling selections +-------------------------------- + +The current selection can be stored in memory with the command ``select -set +<name>``. It can later be recalled using ``select @<name>``. In fact, the +``@<name>`` expression pushes the stored selection on the stack maintained by +the ``select`` command. So for example + +.. code-block:: yoscrypt + + select @foo @bar %i + +will select the intersection between the stored selections ``foo`` and ``bar``. + +In larger investigation efforts it is highly recommended to maintain a +script that sets up relevant selections, so they can easily be recalled, +for example when Yosys needs to be re-run after a design or source code +change. + +The ``history`` command can be used to list all recent interactive commands. +This feature can be useful for creating such a script from the commands +used in an interactive session. + +.. _poke: + +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. + +:numref:`submod` shows how the ``submod`` command can be used to split the +circuit from :numref:`memdemo_src` and :numref:`memdemo_00` into its components. +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. + +.. figure:: ../../images/011/submod_dots.* + :class: width-helper + :name: submod_dots + +.. code-block:: yoscrypt + :caption: The circuit from :numref:`memdemo_src` and :numref:`memdemo_00` + broken up using ``submod`` + :name: submod + + select -set outstage y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff + select -set selstage y %ci2:+$dff[Q,D] %ci*:-$dff @outstage %d + select -set scramble mem* %ci2 %ci*:-$dff mem* %d @selstage %d + submod -name scramble @scramble + submod -name outstage @outstage + submod -name selstage @selstage + +Evaluation of combinatorial circuits +------------------------------------ + +The ``eval`` command can be used to evaluate combinatorial circuits. For example +(see :numref:`submod` for the circuit diagram of ``selstage``): + +:: + + 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 ``eval`` command (as well as the ``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 ``flatten`` +command must be used on modules that instantiate other modules before this +commands can be applied. + +Solving combinatorial SAT problems +---------------------------------- + +.. literalinclude:: ../../../manual/APPNOTE_011_Design_Investigation/primetest.v + :language: verilog + :caption: A simple miter circuit for testing if a number is prime. But it has + a problem (see main text and :numref:`primesat`). + :name: primetest + +.. code-block:: + :caption: Experiments with the miter circuit from :numref:`primetest`. + The first attempt of proving that 31 is prime failed because the + SAT solver found a creative way of factorizing 31 using integer + overflow. + :name: primesat + + yosys [primetest]> sat -prove ok 1 -set p 31 + + 8. 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 + + yosys [primetest]> sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0 + + 9. 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! + + /$$$$$$ /$$$$$$$$ /$$$$$$$ + /$$__ $$ | $$_____/ | $$__ $$ + | $$ \ $$ | $$ | $$ \ $$ + | $$ | $$ | $$$$$ | $$ | $$ + | $$ | $$ | $$__/ | $$ | $$ + | $$/$$ $$ | $$ | $$ | $$ + | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$ + \____ $$$|__/|________/|__/|_______/|__/ + \__/ + +Often the opposite of the ``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 ``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/ + +The ``sat`` command works very similar to the ``eval`` command. The main +difference is that it is now also possible to set output values and find the +corresponding input values. For Example: + +:: + + 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 ``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.) + +: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. + +The Yosys shell session shown in :numref:`primesat` 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 ``sat`` call, as is done in +the second command in :numref:`primesat` (line 31). + +The ``-prove`` option used in this example 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 +------------------------------- + +.. code-block:: + :caption: Solving a sequential SAT problem in the ``memdemo`` module from :numref:`memdemo_src`. + :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 + + 6. 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 + +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 entire memdemo module from :numref:`memdemo_src` 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. :numref:`memdemo_sat` show the solution +to this question, as produced by the following command: + +.. 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 ``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 ``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 ``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. + +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 ``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. + +.. _conclusion: + +Conclusion +========== + +Yosys provides a wide range of functions to analyze and investigate +designs. For many cases it is sufficient to simply display circuit +diagrams, maybe use some additional commands to narrow the scope of the +circuit diagrams to the interesting parts of the circuit. But some cases +require more than that. For this applications Yosys provides commands +that can be used to further inspect the behavior of the circuit, either +by evaluating which output values are generated from certain input +values (``eval``) or by evaluation which input values and initial conditions +can result in a certain behavior at the outputs (``sat``). The SAT command +can even be used to prove (or disprove) theorems regarding the circuit, +in more advanced cases with the additional help of a miter circuit. + +This features can be powerful tools for the circuit designer using Yosys +as a utility for building circuits and the software developer using +Yosys as a framework for new algorithms alike. |