3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-12 04:03:45 +00:00

docs: initial 011 selections move

Also deleting the 011 document.
This commit is contained in:
Krystine Sherwin 2023-10-10 12:36:10 +13:00
parent a019c26b9d
commit 9e35848c8e
No known key found for this signature in database
3 changed files with 268 additions and 323 deletions

View file

@ -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

View file

@ -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
<name>``. It can later be recalled using ``select @<name>``. In fact, the
``@<name>`` 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.

View file

@ -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
<name>``. It can later be recalled using ``select @<name>``. In fact, the
``@<name>`` 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.