mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-07 06:33:24 +00:00
Code Activity

Docs: Shorten cmd:ref

Browse source
This commit is contained in:
Krystine Sherwin 2024-05-03 13:16:48 +12:00
parent e4ec3717bc
commit 829e02ec5b
No known key found for this signature in database
22 changed files with 296 additions and 297 deletions
Download patch file Download diff file Expand all files Collapse all files

104
docs/source/using_yosys/more_scripting/interactive_investigation.rst
View file

@ -13,7 +13,7 @@ A look at the show command
.. TODO:: merge into :doc:`/getting_started/scripting_intro` show section
This section explores the :cmd:ref:`show` command and explains the symbols used
This section explores the `show` command and explains the symbols used
in the circuit diagrams generated by it. The code used is included in the Yosys
code base under |code_examples/show|_.
@ -24,7 +24,7 @@ A simple circuit
^^^^^^^^^^^^^^^^
:ref:`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.
will use to demonstrate the usage of `show` in a simple setting.
.. literalinclude:: /code_examples/show/example.v
:language: Verilog
@ -32,7 +32,7 @@ will use to demonstrate the usage of :cmd:ref:`show` in a simple setting.
: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``
:numref:`example_ys`. Note that `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
@ -58,7 +58,7 @@ is shown.
.. figure:: /_images/code_examples/show/example_first.*
:class: width-helper invert-helper
Output of the first :cmd:ref:`show` command in :numref:`example_ys`
Output of the first `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
@ -84,39 +84,39 @@ 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
The `proc` command transforms the process from the first diagram into a
multiplexer and a d-type flip-flop, which brings us to the second diagram:
.. figure:: /_images/code_examples/show/example_second.*
:class: width-helper invert-helper
Output of the second :cmd:ref:`show` command in :numref:`example_ys`
Output of the second `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
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
``BUF``-node. These are artefacts left behind by the `proc` command. It
is quite usual to see such artefacts after calling commands that perform changes
in the design, as most commands only care about doing the transformation in the
least complicated way, not about cleaning up after them. The next call to
:cmd:ref:`clean` (or :cmd:ref:`opt`, which includes :cmd:ref:`clean` as one of
`clean` (or `opt`, which includes `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`.
call `clean` before calling `show`.
In this script we directly call :cmd:ref:`opt` as the next step, which finally
In this script we directly call `opt` as the next step, which finally
leads us to the third diagram:
.. figure:: /_images/code_examples/show/example_third.*
:class: width-helper invert-helper
:name: example_out
Output of the third :cmd:ref:`show` command in :ref:`example_ys`
Output of the third `show` command in :ref:`example_ys`
Here we see that the :cmd:ref:`opt` command not only has removed the artifacts
left behind by :cmd:ref:`proc`, but also determined correctly that it can remove
Here we see that the `opt` command not only has removed the artifacts
left behind by `proc`, but also determined correctly that it can remove
the first `$mux` cell without changing the behavior of the circuit.
Break-out boxes for signal vectors
@ -129,7 +129,7 @@ accesses.
:caption: :file:`splice.v`
:name: splice_src
Notice how the output for this circuit from the :cmd:ref:`show` command
Notice how the output for this circuit from the `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
@ -169,7 +169,7 @@ mapped to a cell library:
:name: first_pitfall
A half-adder built from simple CMOS gates, demonstrating common pitfalls when
using :cmd:ref:`show`
using `show`
.. literalinclude:: /code_examples/show/cmos.ys
:language: yoscrypt
@ -188,7 +188,7 @@ individual bits, resulting in an unnecessary complex diagram.
:class: width-helper invert-helper
:name: second_pitfall
Effects of :cmd:ref:`splitnets` command and of providing a cell library on
Effects of `splitnets` command and of providing a cell library on
design in :numref:`first_pitfall`
.. literalinclude:: /code_examples/show/cmos.ys
@ -201,11 +201,11 @@ individual bits, resulting in an unnecessary complex diagram.
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>``
passed directly to the `show` command using the ``-lib <filename>``
option. Secondly it is possible to load cell libraries into the design with the
:yoscrypt:`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.
used in all subsequent calls to the `show` command.
In addition to that, :numref:`second_pitfall` was generated after
:yoscrypt:`splitnet -ports` was run on the design. This command splits all
@ -216,7 +216,7 @@ 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
Per default the `show` command outputs a temporary dot file and
launches ``xdot`` to display it. The options ``-format``, ``-viewer`` and
``-prefix`` can be used to change format, viewer and filename prefix. Note that
the ``pdf`` and ``ps`` format are the only formats that support plotting
@ -225,13 +225,13 @@ modules, however ``xdot`` will raise an error when trying to read them.
In densely connected circuits it is sometimes hard to keep track of the
individual signal wires. For these cases it can be useful to call
:cmd:ref:`show` with the ``-colors <integer>`` argument, which randomly assigns
`show` with the ``-colors <integer>`` argument, which randomly assigns
colors to the nets. The integer (> 0) is used as seed value for the random color
assignments. Sometimes it is necessary it try some values to find an assignment
of colors that looks good.
The command :yoscrypt:`help show` prints a complete listing of all options
supported by the :cmd:ref:`show` command.
supported by the `show` command.
Navigating the design
~~~~~~~~~~~~~~~~~~~~~
@ -245,9 +245,9 @@ 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`.
`techmap` command already fails to verify, it is better to troubleshoot
the coarse-grain version of the circuit before `techmap` than the
gate-level circuit after `techmap`.
.. Note::
@ -260,16 +260,16 @@ 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
been identified, it is recommended to simply add the `shell` command to
the matching place in the synthesis script. This command will stop the synthesis
at the specified moment and go to shell mode, where the user can interactively
enter commands.
For most cases, the shell will start with the whole design selected (i.e. when
the synthesis script does not already narrow the selection). The command
: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 :cmd:ref:`ls` command lists the objects within that
`ls` can now be used to create a list of all modules. The command
`cd` can be used to switch to one of the modules (type ``cd ..`` to
switch back). Now the `ls` command lists the objects within that
module. This is demonstrated below using :file:`example.v` from `A simple
circuit`_:
@ -277,10 +277,10 @@ circuit`_:
:language: doscon
:start-at: yosys> ls
:end-before: yosys [example]> dump
:caption: Output of :cmd:ref:`ls` and :cmd:ref:`cd` after running :file:`yosys example.v`
:caption: Output of `ls` and `cd` after running :file:`yosys example.v`
:name: lscd
When a module is selected using the :cmd:ref:`cd` command, all commands (with a
When a module is selected using the `cd` command, all commands (with a
few exceptions, such as the ``read_`` and ``write_`` commands) operate only on
the selected module. This can also be useful for synthesis scripts where
different synthesis strategies should be applied to different modules in the
@ -293,12 +293,12 @@ 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` command. But it is also possible to work from the design-context
(``cd ..``). In this case all object names must be prefixed with
``<module_name>/``. For example ``a*/b*`` would refer to all objects whose names
start with ``b`` from all modules whose names start with ``a``.
The :cmd:ref:`dump` command can be used to print all information about an
The `dump` command can be used to print all information about an
object. For example, calling :yoscrypt:`dump $2` after the :yoscrypt:`cd
example` above:
@ -323,10 +323,10 @@ 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`
- Commands such as `submod`, `expose`, and `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
- Commands such as `eval` and `sat` can be used to investigate
the behavior of the circuit.
- :doc:`/cmd/show`.
- :doc:`/cmd/dump`.
@ -342,10 +342,10 @@ The code used is included in the Yosys code base under
Changing design hierarchy
^^^^^^^^^^^^^^^^^^^^^^^^^
Commands such as :cmd:ref:`flatten` and :cmd:ref:`submod` can be used to change
Commands such as `flatten` and `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
engineering and analysis. An example using `submod` is shown below for
reorganizing a module in Yosys and checking the resulting circuit.
.. literalinclude:: /code_examples/scrambler/scrambler.v
@ -388,7 +388,7 @@ Analyzing the resulting circuit with :doc:`/cmd/eval`:
Behavioral changes
^^^^^^^^^^^^^^^^^^
Commands such as :cmd:ref:`techmap` can be used to make behavioral changes to
Commands such as `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).
@ -425,7 +425,7 @@ Yosys script for ASIC synthesis of the Amber ARMv2 CPU.
endmodule
For more on the :cmd:ref:`techmap` command, see the page on
For more on the `techmap` command, see the page on
:doc:`/yosys_internals/techmap`.
Advanced investigation techniques
@ -448,12 +448,12 @@ Recall the ``memdemo`` design from :ref:`advanced_logic_cones`:
Because this produces a rather large circuit, it can be useful to split it into
smaller parts for viewing and working with. :numref:`submod` does exactly that,
utilising the :cmd:ref:`submod` command to split the circuit into three
utilising the `submod` command to split the circuit into three
sections: ``outstage``, ``selstage``, and ``scramble``.
.. literalinclude:: /code_examples/selections/submod.ys
:language: yoscrypt
:caption: Using :cmd:ref:`submod` to break up the circuit from :file:`memdemo.v`
:caption: Using `submod` to break up the circuit from :file:`memdemo.v`
:start-after: cd memdemo
:end-before: cd ..
:name: submod
@ -481,7 +481,7 @@ below.
Evaluation of combinatorial circuits
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The :cmd:ref:`eval` command can be used to evaluate combinatorial circuits. As
The `eval` command can be used to evaluate combinatorial circuits. As
an example, we will use the ``selstage`` subnet of ``memdemo`` which we found
above and is shown in :numref:`selstage`.
@ -526,20 +526,20 @@ The ``-table`` option can be used to create a truth table. For example:
Assumed undef (x) value for the following signals: \s2
Note that the :cmd:ref:`eval` command (as well as the :cmd:ref:`sat` command
Note that the `eval` command (as well as the `sat` command
discussed in the next sections) does only operate on flattened modules. It can
not analyze signals that are passed through design hierarchy levels. So the
:cmd:ref:`flatten` command must be used on modules that instantiate other
`flatten` command must be used on modules that instantiate other
modules before these commands can be applied.
Solving combinatorial SAT problems
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Often the opposite of the :cmd:ref:`eval` command is needed, i.e. the circuits
Often the opposite of the `eval` command is needed, i.e. the circuits
output is given and we want to find the matching input signals. For small
circuits with only a few input bits this can be accomplished by trying all
possible input combinations, as it is done by the ``eval -table`` command. For
larger circuits however, Yosys provides the :cmd:ref:`sat` command that uses a
larger circuits however, Yosys provides the `sat` command that uses a
`SAT`_ solver, `MiniSAT`_, to solve this kind of problems.
.. _SAT: http://en.wikipedia.org/wiki/Circuit_satisfiability
@ -551,7 +551,7 @@ larger circuits however, Yosys provides the :cmd:ref:`sat` command that uses a
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 `sat` command works very similar to the `eval` command.
The main difference is that it is now also possible to set output values and
find the corresponding input values. For Example:
@ -580,7 +580,7 @@ find the corresponding input values. For Example:
\s1 0 0 00
\s2 0 0 00
Note that the :cmd:ref:`sat` command supports signal names in both arguments to
Note that the `sat` command supports signal names in both arguments to
the ``-set`` option. In the above example we used ``-set s1 s2`` to constraint
``s1`` and ``s2`` to be equal. When more complex constraints are needed, a
wrapper circuit must be constructed that checks the constraints and signals if
@ -642,7 +642,7 @@ 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
the upper 8 bits of ``a`` and ``b`` to zero for the `sat` call, as is
done below.
.. todo:: replace inline code
@ -705,16 +705,16 @@ command:
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
The ``-seq 6`` option instructs the `sat` command to solve a sequential
problem in 6 time steps. (Experiments with lower number of steps have show that
at least 3 cycles are necessary to bring the circuit in a state from which the
sequence 1, 2, 3 can be produced.)
The ``-set-init-undef`` option tells the :cmd:ref:`sat` command to initialize
The ``-set-init-undef`` option tells the `sat` command to initialize
all registers to the undef (``x``) state. The way the ``x`` state is treated in
Verilog will ensure that the solution will work for any initial state.
The ``-max_undef`` option instructs the :cmd:ref:`sat` command to find a
The ``-max_undef`` option instructs the `sat` command to find a
solution with a maximum number of undefs. This way we can see clearly which
inputs bits are relevant to the solution.
@ -807,7 +807,7 @@ 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
There is much more to write about the `sat` command. For example, there
is a set of options that can be used to performs sequential proofs using
temporal induction :cite:p:`een2003temporal`. The command ``help sat`` can be
used to print a list of all options with short descriptions of their functions.

2
docs/source/using_yosys/more_scripting/model_checking.rst
View file

@ -17,7 +17,7 @@ passes in Yosys.
Other applications include checking if a module conforms to interface standards.
The :cmd:ref:`sat` command in Yosys can be used to perform Symbolic Model
The `sat` command in Yosys can be used to perform Symbolic Model
Checking.
Checking techmap

30
docs/source/using_yosys/more_scripting/selections.rst
View file

@ -9,7 +9,7 @@ The selection framework
.. todo:: reduce overlap with :doc:`/getting_started/scripting_intro` select section
The :cmd:ref:`select` command can be used to create a selection for subsequent
The `select` command can be used to create a selection for subsequent
commands. For example:
.. code:: yoscrypt
@ -17,7 +17,7 @@ commands. For example:
select foobar # select the module foobar
delete # delete selected objects
Normally the :cmd:ref:`select` command overwrites a previous selection. The
Normally the `select` command overwrites a previous selection. The
commands :yoscrypt:`select -add` and :yoscrypt:`select -del` can be used to add
or remove objects from the current selection.
@ -26,16 +26,16 @@ default, which is a complete selection of everything in the current module.
This selection framework can also be used directly in many other commands.
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
means that it will use the engine behind the `select` command to
evaluate additional arguments and use the resulting selection instead of the
selection created by the last :cmd:ref:`select` command.
selection created by the last `select` command.
For example, the command :cmd:ref:`delete` will delete everything in the current
For example, the command `delete` will delete everything in the current
selection; while :yoscrypt:`delete foobar` will only delete the module foobar.
If no :cmd:ref:`select` command has been made, then the "current selection" will
If no `select` command has been made, then the "current selection" will
be the whole design.
.. note:: Many of the examples on this page make use of the :cmd:ref:`show`
.. note:: Many of the examples on this page make use of the `show`
command to visually demonstrate the effect of selections. For a more
detailed look at this command, refer to :ref:`interactive_show`.
@ -59,7 +59,7 @@ Module and design context
^^^^^^^^^^^^^^^^^^^^^^^^^
Commands can be executed in *module/* or *design/* context. Until now, all
commands have been executed in design context. The :cmd:ref:`cd` command can be
commands have been executed in design context. The `cd` command can be
used to switch to module context.
In module context, all commands only effect the active module. Objects in the
@ -101,7 +101,7 @@ Operations on selections
Combining selections
^^^^^^^^^^^^^^^^^^^^
The :cmd:ref:`select` command is actually much more powerful than it might seem
The `select` command is actually much more powerful than it might seem
at first glance. 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
@ -190,7 +190,7 @@ 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.
in the stack maintained by the `select` command.
As with the ``%x`` action, these commands broaden the selection by one "step".
But this time the operation only works against the direction of data flow. That
@ -222,9 +222,9 @@ The following sequence of diagrams demonstrates this step-wise expansion:
Notice the subtle difference between :yoscrypt:`show prod %ci` and
:yoscrypt:`show prod %ci %ci`. Both images show the `$mul` cell driven by
some inputs ``$3_Y`` and ``c``. However it is not until the second image,
having called ``%ci`` the second time, that :cmd:ref:`show` is able to
having called ``%ci`` the second time, that `show` is able to
distinguish between ``$3_Y`` being a wire and ``c`` being an input. We can see
this better with the :cmd:ref:`dump` command instead:
this better with the `dump` command instead:
.. literalinclude:: /code_examples/selections/sumprod.out
:language: RTLIL
@ -276,7 +276,7 @@ look at the first section:
This loads :numref:`memdemo_src` and synthesizes the included module. Note that
this code can be copied and run directly in a Yosys command line session,
provided :file:`memdemo.v` is in the same directory. We can now change to the
``memdemo`` module with ``cd memdemo``, and call :cmd:ref:`show` to see the
``memdemo`` module with ``cd memdemo``, and call `show` to see the
diagram in :numref:`memdemo_00`.
.. figure:: /_images/code_examples/selections/memdemo_00.*
@ -387,14 +387,14 @@ 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 :yoscrypt:`select @foo @bar %i`
the `select` command. So for example :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
The `history` command can be used to list all recent interactive
commands. This feature can be useful for creating such a script from the
commands used in an interactive session.