diff --git a/docs/source/appendix.rst b/docs/source/appendix.rst index 87581793b..04ee2945c 100644 --- a/docs/source/appendix.rst +++ b/docs/source/appendix.rst @@ -10,7 +10,6 @@ Appendix appendix/auxprogs appendix/APPNOTE_010_Verilog_to_BLIF.rst - appendix/APPNOTE_011_Design_Investigation.rst appendix/APPNOTE_012_Verilog_to_BTOR.rst bib diff --git a/docs/source/appendix/APPNOTE_011_Design_Investigation.rst b/docs/source/appendix/APPNOTE_011_Design_Investigation.rst deleted file mode 100644 index 3cbd0eb90..000000000 --- a/docs/source/appendix/APPNOTE_011_Design_Investigation.rst +++ /dev/null @@ -1,322 +0,0 @@ -========================================== -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. - -.. _Yosys GIT: https://github.com/YosysHQ/yosys - -.. _Rev. 2b90ba1: https://github.com/YosysHQ/yosys/tree/2b90ba1 - -Overview -======== - -This application note is structured as follows: - -: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:`conclusion` concludes the document and summarizes the key points. - -.. _navigate: - -Navigating the design -===================== - -Interactive navigation ----------------------- - -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 :cmd:ref:`show` after ``select $2`` or ``select t:$add`` (see also - :numref:`example_out`) - -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. - -For example, if the command ``select $2`` is executed, a subsequent -:cmd:ref:`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:: ../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 :cmd:ref:`select` command to -evaluate additional arguments and use the resulting selection instead of the -selection created by the last :cmd:ref:`select` command. - -Normally the :cmd:ref:`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:: ../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 :cmd:ref:`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 :cmd:ref:`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 :cmd:ref:`show` now we -see the diagram shown in :numref:`memdemo_00`. - -.. literalinclude:: ../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 -``. It can later be recalled using ``select @``. In fact, the -``@`` expression pushes the stored selection on the stack maintained by -the :cmd:ref:`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 :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. - -.. _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 (:cmd:ref:`eval`) or by evaluation which -input values and initial conditions can result in a certain behavior at the -outputs (:cmd:ref:`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. diff --git a/docs/source/using_yosys/more_scripting/selections.rst b/docs/source/using_yosys/more_scripting/selections.rst index b51ea34ea..b1a07ca01 100644 --- a/docs/source/using_yosys/more_scripting/selections.rst +++ b/docs/source/using_yosys/more_scripting/selections.rst @@ -185,3 +185,271 @@ Example: .. figure:: /_images/res/PRESENTATION_ExAdv/select.* :class: width-helper + +.. todo:: combine below sections into above where possible + +Working with selections +~~~~~~~~~~~~~~~~~~~~~~~ + +.. figure:: /_images/011/example_03.* + :class: width-helper + :name: seladd + + Output of :cmd:ref:`show` after ``select $2`` or ``select t:$add`` (see also + :numref:`example_out`) + +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. + +For example, if the command ``select $2`` is executed, a subsequent +:cmd:ref:`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:: ../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 :cmd:ref:`select` command to +evaluate additional arguments and use the resulting selection instead of the +selection created by the last :cmd:ref:`select` command. + +Normally the :cmd:ref:`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:: ../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 :cmd:ref:`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 :cmd:ref:`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 :cmd:ref:`show` now we +see the diagram shown in :numref:`memdemo_00`. + +.. literalinclude:: ../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 +``. It can later be recalled using ``select @``. In fact, the +``@`` expression pushes the stored selection on the stack maintained by +the :cmd:ref:`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 :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.