Rst docs conversion (#3496)

Rst docs conversion

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.