riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

docs: Tidying interactive investigation 

More :numref: because I figured out they were only failing if I didn't do a full re-make.
Reflow first section a little to help readability.
Also includes a css change to prevent code block caption text from bunching into the caption number.
This commit is contained in:
Krystine Sherwin 2023-10-11 11:13:06 +13:00
parent 9e35848c8e
commit c61ab7d627
No known key found for this signature in database
2 changed files with 91 additions and 63 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
docs/source/_static/custom.css
View File

@ -12,4 +12,9 @@
/* Make images full width */
.width-helper {
max-width: 100%;
}
}
/* Prevent code block caption text from bunching into the caption number */
.literal-block-wrapper .code-block-caption .caption-number {
padding-right: 0.5em
}

147
docs/source/using_yosys/more_scripting/interactive_investigation.rst
View File

@ -1,26 +1,38 @@
Interactive design investigation
--------------------------------
.. role:: yoscrypt(code)
:language: yoscrypt
.. _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.
This section explores 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.
:numref:`example_v` below provides the Verilog code for a simple circuit which
we will use to demonstrate the usage of :cmd:ref:`show` in a simple setting.
.. literalinclude:: /APPNOTE_011_Design_Investigation/example.v
:language: Verilog
:caption: ``docs/source/APPNOTE_011_Design_Investigation/example.v``
:name: example_v
The Yosys synthesis script we will be running is included as
:numref:`example_ys`. 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. Using :yoscrypt:`show -pause` 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``
:name: example_ys
read_verilog example.v
show -pause # first
@ -29,17 +41,14 @@ continuing synthesis.
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.
synthesis commands. We will now look at each of these diagrams and explain what
is shown.
.. figure:: /_images/011/example_00.*
:class: width-helper
Output of the first :cmd:ref:`show` command above
Output of the first :cmd:ref:`show` command in :numref:`example_ys`
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
@ -71,7 +80,7 @@ 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
Output of the second :cmd:ref:`show` command in :numref:`example_ys`
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
@ -94,7 +103,7 @@ leads us to the third diagram:
:class: width-helper
:name: example_out
Output of the third :cmd:ref:`show` command above
Output of the third :cmd:ref:`show` command in :numref:`example_ys`
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
@ -110,12 +119,12 @@ accesses.
: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.
Notice how the output for this circuit from the :cmd:ref:`show` command
(:numref:`splice_dia`) 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
@ -142,11 +151,15 @@ Yosys commands.
Gate level netlists
^^^^^^^^^^^^^^^^^^^
The diagram below shows two common pitfalls when working with
designs mapped to a cell library:
:numref:`first_pitfall` shows two common pitfalls when working with designs
mapped to a cell library:
.. figure:: /_images/011/cmos_00.*
:class: width-helper
:name: first_pitfall
A half-adder built from simple CMOS gates, demonstrating common pitfalls when
using :cmd:ref:`show`
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
@ -156,24 +169,25 @@ individual bits, resulting in an unnecessary complex diagram.
.. figure:: /_images/011/cmos_01.*
:class: width-helper
:name: second_pitfall
Effects of :cmd:ref:`splitnets` command and of providing a cell library. (The
circuit is a half-adder built from simple CMOS gates.)
Effects of :cmd:ref:`splitnets` command and of providing a cell library on
design in :numref:`first_pitfall`
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
For :numref:`second_pitfall`, 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 <filename>``
option. Secondly it is possible to load cell libraries into the design with the
``read_verilog -lib <filename>`` 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.
In addition to that, :numref:`second_pitfall` 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
^^^^^^^^^^^^^^^^^^^
@ -228,11 +242,14 @@ 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`:
switch back). Now the `ls` command lists the objects within that module.
:numref:`lscd` below demonstrates this using the ``example.v`` from
`A simple circuit`_
.. todo:: update yosys output with $ternary$example.v$3
.. code-block:: none
:caption: Demonstration of :cmd:ref:`ls` and :cmd:ref:`cd`
:caption: Demonstration of :cmd:ref:`ls` and :cmd:ref:`cd` having run ``yosys example.v``
:name: lscd
yosys> ls
@ -264,8 +281,8 @@ 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
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.
@ -277,12 +294,12 @@ Usually all interactive work is done with one module selected using the
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.
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.
.. code-block:: RTLIL
:caption: Output of ``dump $2`` using the design from ``example.v``
:caption: Output of ``dump $2`` using ``example.v`` from `A simple circuit`_
:name: dump2
attribute \src "example.v:5"
@ -420,8 +437,9 @@ 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
:name: memdemo_v
Let's consider the design above. It serves no purpose other than being a
Let's consider :numref:`memdemo_v`. 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
@ -433,7 +451,7 @@ the following diagram:
``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,
smaller parts for viewing and working with. :numref:`submod` does exactly that,
utilising the :cmd:ref:`submod` command to split the circuit into three
sections: ``outstage``, ``selstage``, and ``scramble``.
@ -459,6 +477,7 @@ below.
.. figure:: /_images/011/submod_03.*
:class: width-helper
:name: selstage
``selstage``
@ -472,7 +491,7 @@ 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.
above and is shown in :numref:`selstage`.
::
@ -580,12 +599,13 @@ circuit.)
prime. But it has a problem.
:name: primetest
The code above shows a miter circuit that is supposed to be used as a prime
: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.
.. code-block::
:caption: Experiments with the miter circuit from ``primetest.v``.
:name: prime_shell
yosys [primetest]> sat -prove ok 1 -set p 31
@ -617,18 +637,20 @@ number test. If ``ok`` is 1 for all input values ``a`` and ``b`` for a given
\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.
The Yosys shell session shown in :numref:`prime_shell` 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.
:name: prime_fixed
yosys [primetest]> sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0
@ -656,10 +678,10 @@ to zero for the :cmd:ref:`sat` call, as is done below.
\____ $$$|__/|________/|__/|_______/|__/
\__/
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.
The ``-prove`` option used in :numref:`prime_fixed` 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
@ -671,9 +693,10 @@ 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:
the entire memdemo module from ``memdemo.v`` (:numref:`memdemo_v` above) 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