diff --git a/docs/source/appendix/APPNOTE_011_Design_Investigation.rst b/docs/source/appendix/APPNOTE_011_Design_Investigation.rst index 5552408cc..3cbd0eb90 100644 --- a/docs/source/appendix/APPNOTE_011_Design_Investigation.rst +++ b/docs/source/appendix/APPNOTE_011_Design_Investigation.rst @@ -6,323 +6,31 @@ 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 :cmd:ref:`show` -command requires a working installation of `GraphViz`_ and `xdot` for generating -the actual circuit diagrams. +2013-12-08. The README file covers how to install Yosys. .. _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 :cmd:ref:`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 :cmd:ref:`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 :cmd:ref:`show` commands from :numref:`example_src` - -The :cmd:ref:`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 :cmd:ref:`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 -``'`` 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 :cmd:ref:`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 :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:`proc`, which includes :cmd:ref:`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 :cmd:ref:`clean` before calling :cmd:ref:`show`. - -In this script we directly call :cmd:ref:`proc` as next step, which finally -leads us to the 3rd diagram in :numref:`example_out`. 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. - -.. figure:: /_images/011/splice.* - :class: width-helper - :name: splice_dia - - Output of ``yosys -p 'proc; opt; show' splice.v`` - -.. literalinclude:: ../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 :cmd:ref:`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 :cmd:ref:`show` in :numref:`splice_src` -demonstrates how such circuits are visualized by the :cmd:ref:`show` command. - -The key elements in understanding this circuit diagram are of course the boxes -with round corners and rows labeled ``: - -:``. Each of this boxes has one signal per row on one side -and a common signal for all rows on the other side. The ``:`` 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 :cmd:ref:`show` command using the ``-lib `` -option. Secondly it is possible to load cell libraries into the design with the -``read_verilog -lib `` 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 :cmd:ref:`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 :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. - -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 :cmd:ref:`show` -with the ``-colors `` 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 :cmd:ref:`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 -: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 ``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 :cmd:ref:`ls` and :cmd:ref:`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 :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 `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 -: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 -``/``. 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 ``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. @@ -336,12 +44,6 @@ Working with selections Output of :cmd:ref:`show` after ``select $2`` or ``select t:$add`` (see also :numref:`example_out`) -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. - But for most interactive work we want to further narrow the set of selected objects. This can be done using the :cmd:ref:`select` command. @@ -598,352 +300,6 @@ The :cmd:ref:`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 :cmd:ref:`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 :cmd:ref:`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 :cmd:ref:`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 :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 this commands can be applied. - -Solving combinatorial SAT problems ----------------------------------- - -.. literalinclude:: ../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 :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/ - -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: - -:: - - 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.) - -: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 :cmd:ref:`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 :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. - -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. - .. _conclusion: Conclusion diff --git a/docs/source/getting_started/installation.rst b/docs/source/getting_started/installation.rst index 0b7f52b1d..1677445fa 100644 --- a/docs/source/getting_started/installation.rst +++ b/docs/source/getting_started/installation.rst @@ -1,6 +1,8 @@ Installation ------------ +.. todo:: update and finish installation instructions + Supported platforms ~~~~~~~~~~~~~~~~~~~ diff --git a/docs/source/getting_started/scripting_intro.rst b/docs/source/getting_started/scripting_intro.rst index 9ebdc1d9d..35015ceb9 100644 --- a/docs/source/getting_started/scripting_intro.rst +++ b/docs/source/getting_started/scripting_intro.rst @@ -98,6 +98,8 @@ Commands for model checking: Selections intro ~~~~~~~~~~~~~~~~ +.. todo:: reorder text for logical consistency + Most commands can operate not only on the entire design but also specifically on selected parts of the design. For example the command :cmd:ref:`dump` will print all selected objects in the current design while ``dump foobar`` will only print @@ -113,3 +115,52 @@ print all wires that are connected to the ``\A`` port of a ``$add`` cell. Detailed documentation of the select framework can be found under :doc:`/using_yosys/more_scripting/selections` or in the command reference at :doc:`/cmd/select`. + +The show command +~~~~~~~~~~~~~~~~ + +The :cmd:ref:`show` command requires a working installation of `GraphViz`_ and +`xdot`_ for generating the actual circuit diagrams. Below is an example of how +this command can be used, showing the changes in the generated circuit at +different stages of the yosys tool flow. + +.. _GraphViz: http://www.graphviz.org/ + +.. _xdot: https://github.com/jrfonseca/xdot.py + +.. code-block:: console + :caption: Yosys script with :cmd:ref:`show` commands and example design + :name: show_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: show_out + + Output of the three :cmd:ref:`show` commands from :numref:`show_src` + +A circuit diagram is generated 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). + +For more information on the :cmd:ref:`show` command, including a guide on what +the different symbols represent, see :ref:`interactive_show` and the +:doc:`/using_yosys/more_scripting/interactive_investigation` page. diff --git a/docs/source/using_yosys/more_scripting/index.rst b/docs/source/using_yosys/more_scripting/index.rst index 32879c0d4..8fb460613 100644 --- a/docs/source/using_yosys/more_scripting/index.rst +++ b/docs/source/using_yosys/more_scripting/index.rst @@ -6,5 +6,6 @@ More scripting opt_passes selections + interactive_investigation synth troubleshooting diff --git a/docs/source/using_yosys/more_scripting/interactive_investigation.rst b/docs/source/using_yosys/more_scripting/interactive_investigation.rst new file mode 100644 index 000000000..6eab48bf5 --- /dev/null +++ b/docs/source/using_yosys/more_scripting/interactive_investigation.rst @@ -0,0 +1,786 @@ +Interactive design investigation +-------------------------------- + +.. _interactive_show: + +A look at the show command +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +This section introduces the :cmd:ref:`show` command and explains the symbols +used in the circuit diagrams generated by it. + +A simple circuit +^^^^^^^^^^^^^^^^ + +The code listings below show a simple synthesis script and a Verilog file that +demonstrate the usage of show in a simple setting. 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. The ``show -pause`` command also allows +the user to enter an interactive shell to further investigate the circuit before +continuing synthesis. + +.. code-block:: yoscrypt + :caption: ``docs/source/APPNOTE_011_Design_Investigation/example.ys`` + + read_verilog example.v + show -pause # first + proc + show -pause # second + opt + show -pause # third + +.. literalinclude:: /APPNOTE_011_Design_Investigation/example.v + :language: Verilog + :caption: ``docs/source/APPNOTE_011_Design_Investigation/example.v`` + +This script, when executed, will show the design after each of the three +synthesis commands. + +.. figure:: /_images/011/example_00.* + :class: width-helper + + Output of the first :cmd:ref:`show` command above + +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 +``'`` 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 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-flip, which brings us to the second diagram: + +.. figure:: /_images/011/example_01.* + :class: width-helper + + Output of the second :cmd:ref:`show` command above + +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/011/example_02.* + :class: width-helper + :name: example_out + + Output of the third :cmd:ref:`show` command above + +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:: /APPNOTE_011_Design_Investigation/splice.v + :caption: ``splice.v`` + :name: splice_src + +Notice how the output for this circuit from the :cmd:ref:`show` command below +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/011/splice.* + :class: width-helper + :name: splice_dia + + Output of ``yosys -p 'proc; opt; show' splice.v`` + +The key elements in understanding this circuit diagram are of course the boxes +with round corners and rows labeled ``: - +:``. Each of this boxes has one signal per row on one side +and a common signal for all rows on the other side. The ``:`` 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 +^^^^^^^^^^^^^^^^^^^ + +The diagram below shows two common pitfalls when working with +designs mapped to a cell library: + +.. figure:: /_images/011/cmos_00.* + :class: width-helper + +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/011/cmos_01.* + :class: width-helper + + Effects of :cmd:ref:`splitnets` command and of providing a cell library. (The + circuit is a half-adder built from simple CMOS gates.) + +For the second 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 :cmd:ref:`show` command using the ``-lib `` +option. Secondly it is possible to load cell libraries into the design with the +``read_verilog -lib `` 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, the second 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 :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. + +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 :cmd:ref:`show` +with the ``-colors `` 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 :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 ``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 +^^^^^^^^^^^^^^^^^^^^^^ + +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 `ls` command lists the objects within that module. The +code block below demonstrates this using the design from :ref:`interactive_show`: + +.. code-block:: none + :caption: Demonstration of :cmd:ref:`ls` and :cmd:ref:`cd` + :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 + +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 :ref:`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 +``/``. 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 ``dump $2`` will print the below. 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. + +.. code-block:: RTLIL + :caption: Output of ``dump $2`` using the design from ``example.v`` + :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 + +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. + +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:: ../../../resources/PRESENTATION_ExOth/scrambler.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExOth/scrambler.v`` + +.. code:: yoscrypt + + read_verilog scrambler.v + + hierarchy; proc;; + + cd scrambler + submod -name xorshift32 \ + xs %c %ci %D %c %ci:+[D] %D \ + %ci*:-$dff xs %co %ci %d + +.. figure:: /_images/res/PRESENTATION_ExOth/scrambler_p01.* + :class: width-helper + +.. figure:: /_images/res/PRESENTATION_ExOth/scrambler_p02.* + :class: width-helper + +Analyzing the resulting circuit with :doc:`/cmd/eval`: + +.. 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. + +.. 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 + <= 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. + +.. literalinclude:: /APPNOTE_011_Design_Investigation/memdemo.v + :caption: ``memdemo.v``, a demo circuit for demonstrating some advanced Yosys features + :language: verilog + +Let's consider the design above. 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 :cmd:ref:`show` now we see +the following diagram: + +.. figure:: /_images/011/memdemo_00.* + :class: width-helper + + ``memdemo`` + +Because this produces a rather large circuit, it can be useful to split it into +smaller parts for viewing and working with. The code below does exactly that, +utilising the :cmd:ref:`submod` command to split the circuit into three +sections: ``outstage``, ``selstage``, and ``scramble``. + +.. code-block:: yoscrypt + :caption: The circuit from ``memdemo.v`` broken up using :cmd:ref:`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 + +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/011/submod_02.* + :class: width-helper + + ``outstage`` + +.. figure:: /_images/011/submod_03.* + :class: width-helper + + ``selstage`` + +.. figure:: /_images/011/submod_01.* + :class: width-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. + +:: + + 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 this 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: + +:: + + 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:: /APPNOTE_011_Design_Investigation/primetest.v + :language: verilog + :caption: ``primetest.v``, a simple miter circuit for testing if a number is + prime. But it has a problem. + :name: primetest + +The code above 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. + +.. code-block:: + :caption: Experiments with the miter circuit from ``primetest.v``. + + 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 above 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. + +.. code-block:: + :caption: Miter circuit from ``primetest.v``, with the upper 8 bits of ``a`` + and ``b`` constrained to prevent overflow. + + 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 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 +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +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 ``memdemo.v`` 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: + +.. 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: + +.. 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. diff --git a/docs/source/using_yosys/more_scripting/selections.rst b/docs/source/using_yosys/more_scripting/selections.rst index 2957a1c2f..b51ea34ea 100644 --- a/docs/source/using_yosys/more_scripting/selections.rst +++ b/docs/source/using_yosys/more_scripting/selections.rst @@ -21,7 +21,9 @@ commands. For example: delete # delete selected objects select -clear # reset selection (select whole design) -See :doc:`/cmd/select` +Many of the examples on this page make use of the :cmd:ref:`show` command to +visually demonstrate the effect of selections. For a more detailed look at this +command, refer to :ref:`interactive_show`. How to make a selection ~~~~~~~~~~~~~~~~~~~~~~~ @@ -78,8 +80,8 @@ Special patterns can be used to select by object property or type. For example: A complete list of this pattern expressions can be found in the command reference to the :cmd:ref:`select` command. -Combining selection -^^^^^^^^^^^^^^^^^^^ +Combining selections +^^^^^^^^^^^^^^^^^^^^ When more than one selection expression is used in one statement, then they are pushed on a stack. The final elements on the stack are combined into a union: @@ -183,112 +185,3 @@ Example: .. figure:: /_images/res/PRESENTATION_ExAdv/select.* :class: width-helper - -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. - -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:: ../../../resources/PRESENTATION_ExOth/scrambler.v - :language: verilog - :caption: ``docs/resources/PRESENTATION_ExOth/scrambler.v`` - -.. code:: yoscrypt - - read_verilog scrambler.v - - hierarchy; proc;; - - cd scrambler - submod -name xorshift32 \ - xs %c %ci %D %c %ci:+[D] %D \ - %ci*:-$dff xs %co %ci %d - -.. figure:: /_images/res/PRESENTATION_ExOth/scrambler_p01.* - :class: width-helper - -.. figure:: /_images/res/PRESENTATION_ExOth/scrambler_p02.* - :class: width-helper - -Analyzing the resulting circuit with :doc:`/cmd/eval`: - -.. 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. - -.. 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 - <= D; - - endmodule - -For more on the :cmd:ref:`techmap` command, see the page on -:doc:`/yosys_internals/techmap`.