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

Rst docs conversion (#3496)

Browse source 
Rst docs conversion
This commit is contained in:
KrystalDelusion 2022-11-16 00:55:22 +13:00 • committed by GitHub
parent 853f4bb3c6
commit a14dec79eb
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
57 changed files with 7792 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

336
docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst Normal file
View file

@ -0,0 +1,336 @@
====================================
010: Converting Verilog to BLIF page
====================================
Installation
============
Yosys written in C++ (using features from C++11) and is tested on modern
Linux. It should compile fine on most UNIX systems with a C++11
compiler. The README file contains useful information on building Yosys
and its prerequisites.
Yosys is a large and feature-rich program with a couple of dependencies.
It is, however, possible to deactivate some of the dependencies in the
Makefile, resulting in features in Yosys becoming unavailable. When
problems with building Yosys are encountered, a user who is only
interested in the features of Yosys that are discussed in this
Application Note may deactivate TCL, Qt and MiniSAT support in the
Makefile and may opt against building yosys-abc.
This Application Note is based on `Yosys GIT`_ `Rev. e216e0e`_ from 2013-11-23.
The Verilog sources used for the examples are taken from `yosys-bigsim`_, a
collection of real-world designs used for regression testing Yosys.
.. _Yosys GIT: https://github.com/YosysHQ/yosys
.. _Rev. e216e0e: https://github.com/YosysHQ/yosys/tree/e216e0e
.. _yosys-bigsim: https://github.com/YosysHQ/yosys-bigsim
Getting started
===============
We start our tour with the Navré processor from yosys-bigsim. The `Navré
processor`_ is an Open Source AVR clone. It is a single module (softusb_navre)
in a single design file (softusb_navre.v). It also is using only features that
map nicely to the BLIF format, for example it only uses synchronous resets.
.. _Navré processor: http://opencores.org/projects/navre
Converting softusb_navre.v to softusb_navre.blif could not be easier:
.. code:: sh
yosys -o softusb_navre.blif -S softusb_navre.v
Behind the scenes Yosys is controlled by synthesis scripts that execute
commands that operate on Yosys' internal state. For example, the -o
softusb_navre.blif option just adds the command write_blif
softusb_navre.blif to the end of the script. Likewise a file on the
command line – softusb_navre.v in this case – adds the command
read_verilog softusb_navre.v to the beginning of the synthesis script.
In both cases the file type is detected from the file extension.
Finally the option -S instantiates a built-in default synthesis script.
Instead of using -S one could also specify the synthesis commands for
the script on the command line using the -p option, either using
individual options for each command or by passing one big command string
with a semicolon-separated list of commands. But in most cases it is
more convenient to use an actual script file.
Using a synthesis script
========================
With a script file we have better control over Yosys. The following
script file replicates what the command from the last section did:
.. code:: yoscrypt
read_verilog softusb_navre.v
hierarchy
proc; opt; memory; opt; techmap; opt
write_blif softusb_navre.blif
The first and last line obviously read the Verilog file and write the
BLIF file.
The 2nd line checks the design hierarchy and instantiates parametrized
versions of the modules in the design, if necessary. In the case of this
simple design this is a no-op. However, as a general rule a synthesis
script should always contain this command as first command after reading
the input files.
The 3rd line does most of the actual work:
- The command opt is the Yosys' built-in optimizer. It can perform some
simple optimizations such as const-folding and removing unconnected
parts of the design. It is common practice to call opt after each
major step in the synthesis procedure. In cases where too much
optimization is not appreciated (for example when analyzing a
design), it is recommended to call clean instead of opt.
- The command proc converts processes (Yosys' internal representation
of Verilog always- and initial-blocks) to circuits of multiplexers
and storage elements (various types of flip-flops).
- The command memory converts Yosys' internal representations of arrays
and array accesses to multi-port block memories, and then maps this
block memories to address decoders and flip-flops, unless the option
-nomap is used, in which case the multi-port block memories stay in
the design and can then be mapped to architecture-specific memory
primitives using other commands.
- The command techmap turns a high-level circuit with coarse grain
cells such as wide adders and multipliers to a fine-grain circuit of
simple logic primitives and single-bit storage elements. The command
does that by substituting the complex cells by circuits of simpler
cells. It is possible to provide a custom set of rules for this
process in the form of a Verilog source file, as we will see in the
next section.
Now Yosys can be run with the filename of the synthesis script as
argument:
.. code:: sh
yosys softusb_navre.ys
Now that we are using a synthesis script we can easily modify how Yosys
synthesizes the design. The first thing we should customize is the call
to the hierarchy command:
Whenever it is known that there are no implicit blackboxes in the
design, i.e. modules that are referenced but are not defined, the
hierarchy command should be called with the -check option. This will
then cause synthesis to fail when implicit blackboxes are found in the
design.
The 2nd thing we can improve regarding the hierarchy command is that we
can tell it the name of the top level module of the design hierarchy. It
will then automatically remove all modules that are not referenced from
this top level module.
For many designs it is also desired to optimize the encodings for the
finite state machines (FSMs) in the design. The fsm command finds FSMs,
extracts them, performs some basic optimizations and then generate a
circuit from the extracted and optimized description. It would also be
possible to tell the fsm command to leave the FSMs in their extracted
form, so they can be further processed using custom commands. But in
this case we don't want that.
So now we have the final synthesis script for generating a BLIF file for
the Navré CPU:
.. code:: yoscrypt
read_verilog softusb_navre.v
hierarchy -check -top softusb_navre
proc; opt; memory; opt; fsm; opt; techmap; opt
write_blif softusb_navre.blif
Advanced example: The Amber23 ARMv2a CPU
========================================
Our 2nd example is the `Amber23 ARMv2a CPU`_. Once again we base our example on
the Verilog code that is included in `yosys-bigsim`_.
.. _Amber23 ARMv2a CPU: http://opencores.org/projects/amber
.. code-block:: yoscrypt
:caption: `amber23.ys`
:name: amber23.ys
read_verilog a23_alu.v
read_verilog a23_barrel_shift_fpga.v
read_verilog a23_barrel_shift.v
read_verilog a23_cache.v
read_verilog a23_coprocessor.v
read_verilog a23_core.v
read_verilog a23_decode.v
read_verilog a23_execute.v
read_verilog a23_fetch.v
read_verilog a23_multiply.v
read_verilog a23_ram_register_bank.v
read_verilog a23_register_bank.v
read_verilog a23_wishbone.v
read_verilog generic_sram_byte_en.v
read_verilog generic_sram_line_en.v
hierarchy -check -top a23_core
add -global_input globrst 1
proc -global_arst globrst
techmap -map adff2dff.v
opt; memory; opt; fsm; opt; techmap
write_blif amber23.blif
The problem with this core is that it contains no dedicated reset logic. Instead
the coding techniques shown in :numref:`glob_arst` are used to define reset
values for the global asynchronous reset in an FPGA implementation. This design
can not be expressed in BLIF as it is. Instead we need to use a synthesis script
that transforms this form to synchronous resets that can be expressed in BLIF.
(Note that there is no problem if this coding techniques are used to
model ROM, where the register is initialized using this syntax but is
never updated otherwise.)
:numref:`amber23.ys` shows the synthesis script for the Amber23 core. In line 17
the add command is used to add a 1-bit wide global input signal with the name
globrst. That means that an input with that name is added to each module in the
design hierarchy and then all module instantiations are altered so that this new
signal is connected throughout the whole design hierarchy.
.. code-block:: verilog
:caption: Implicit coding of global asynchronous resets
:name: glob_arst
reg [7:0] a = 13, b;
initial b = 37;
.. code-block:: verilog
:caption: `adff2dff.v`
:name: adff2dff.v
(* 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
Q <= D;
endmodule
In line 18 the proc command is called. But in this script the signal
name globrst is passed to the command as a global reset signal for
resetting the registers to their assigned initial values.
Finally in line 19 the techmap command is used to replace all instances of
flip-flops with asynchronous resets with flip-flops with synchronous resets. The
map file used for this is shown in :numref:`adff2dff.v`. Note how the
techmap_celltype attribute is used in line 1 to tell the techmap command which
cells to replace in the design, how the \_TECHMAP_FAIL\_ wire in lines 15 and 16
(which evaluates to a constant value) determines if the parameter set is
compatible with this replacement circuit, and how the \_TECHMAP_DO\_ wire in
line 13 provides a mini synthesis-script to be used to process this cell.
.. code-block:: c
:caption: Test program for the Amber23 CPU (Sieve of Eratosthenes). Compiled
using GCC 4.6.3 for ARM with ``-Os -marm -march=armv2a
-mno-thumb-interwork -ffreestanding``, linked with ``--fix-v4bx``
set and booted with a custom setup routine written in ARM assembler.
:name: sieve
#include <stdint.h>
#include <stdbool.h>
#define BITMAP_SIZE 64
#define OUTPORT 0x10000000
static uint32_t bitmap[BITMAP_SIZE/32];
static void bitmap_set(uint32_t idx) { bitmap[idx/32] |= 1 << (idx % 32); }
static bool bitmap_get(uint32_t idx) { return (bitmap[idx/32] & (1 << (idx % 32))) != 0; }
static void output(uint32_t val) { *((volatile uint32_t*)OUTPORT) = val; }
int main() {
uint32_t i, j, k;
output(2);
for (i = 0; i < BITMAP_SIZE; i++) {
if (bitmap_get(i)) continue;
output(3+2*i);
for (j = 2*(3+2*i);; j += 3+2*i) {
if (j%2 == 0) continue;
k = (j-3)/2;
if (k >= BITMAP_SIZE) break;
bitmap_set(k);
}
}
output(0);
return 0;
}
Verification of the Amber23 CPU
===============================
The BLIF file for the Amber23 core, generated using :numref:`amber23.ys` and
:numref:`adff2dff.v` and the version of the Amber23 RTL source that is bundled
with yosys-bigsim, was verified using the test-bench from yosys-bigsim. It
successfully executed the program shown in :numref:`sieve` in the test-bench.
For simulation the BLIF file was converted back to Verilog using `ABC`_. So this
test includes the successful transformation of the BLIF file into ABC's internal
format as well.
.. _ABC: https://github.com/berkeley-abc/abc
The only thing left to write about the simulation itself is that it
probably was one of the most energy inefficient and time consuming ways
of successfully calculating the first 31 primes the author has ever
conducted.
Limitations
===========
At the time of this writing Yosys does not support multi-dimensional
memories, does not support writing to individual bits of array elements,
does not support initialization of arrays with $readmemb and $readmemh,
and has only limited support for tristate logic, to name just a few
limitations.
That being said, Yosys can synthesize an overwhelming majority of
real-world Verilog RTL code. The remaining cases can usually be modified
to be compatible with Yosys quite easily.
The various designs in yosys-bigsim are a good place to look for
examples of what is within the capabilities of Yosys.
Conclusion
==========
Yosys is a feature-rich Verilog-2005 synthesis tool. It has many uses,
but one is to provide an easy gateway from high-level Verilog code to
low-level logic circuits.
The command line option -S can be used to quickly synthesize Verilog
code to BLIF files without a hassle.
With custom synthesis scripts it becomes possible to easily perform
high-level optimizations, such as re-encoding FSMs. In some extreme
cases, such as the Amber23 ARMv2 CPU, the more advanced Yosys features
can be used to change a design to fit a certain need without actually
touching the RTL code.

965
docs/source/appendix/APPNOTE_011_Design_Investigation.rst Normal file
View file

@ -0,0 +1,965 @@
==========================================
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. The ``show`` command
requires a working installation of `GraphViz`_ and `xdot` for generating the
actual circuit diagrams.
.. _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 ``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 ``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 ``show`` commands from :numref:`example_src`
The ``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 ``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
``<bit_width>'<bits>`` 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 ``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 ``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
``clean`` (or ``opt``, which includes ``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 ``clean`` before
calling ``show``.
In this script we directly call ``opt`` as next step, which finally leads us to
the 3rd diagram in :numref:`example_out`. 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.
.. figure:: ../../images/011/splice.*
:class: width-helper
:name: splice_dia
Output of ``yosys -p 'proc; opt; show' splice.v``
.. literalinclude:: ../../../manual/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 ``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 ``show`` in :numref:`splice_src` demonstrates
how such circuits are visualized by the ``show`` command.
The key elements in understanding this circuit diagram are of course the boxes
with round corners and rows labeled ``<MSB_LEFT>:<LSB_LEFT> -
<MSB_RIGHT>:<LSB_RIGHT>``. Each of this boxes has one signal per row on one side
and a common signal for all rows on the other side. The ``<MSB>:<LSB>`` 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 ``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 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 ``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 ``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 ``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 ``help show`` prints a complete listing of all options supported by
the ``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 ``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:: 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 ``ls`` and ``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 ``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 ``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. :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 ``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 ``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.
Working with selections
-----------------------
.. figure:: ../../images/011/example_03.*
:class: width-helper
:name: seladd
Output of ``show`` after ``select $2`` or ``select t:$add`` (see also
:numref:`example_out`)
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 design.
But for most interactive work we want to further narrow the set of
selected objects. This can be done using the ``select`` command.
For example, if the command ``select $2`` is executed, a subsequent ``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:: ../../../manual/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 ``select`` command to evaluate
additional arguments and use the resulting selection instead of the selection
created by the last ``select`` command.
Normally the ``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:: ../../../manual/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 ``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 ``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 ``show`` now we see
the diagram shown in :numref:`memdemo_00`.
.. literalinclude:: ../../../manual/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 ``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 ``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 ``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 ``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 ``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 ``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 ``flatten``
command must be used on modules that instantiate other modules before this
commands can be applied.
Solving combinatorial SAT problems
----------------------------------
.. literalinclude:: ../../../manual/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 ``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 ``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 ``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:
::
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 ``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 ``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 ``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 ``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 ``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 ``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
==========
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 (``eval``) or by evaluation which input values and initial conditions
can result in a certain behavior at the outputs (``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.

333
docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst Normal file
View file

@ -0,0 +1,333 @@
====================================
012: Converting Verilog to BTOR page
====================================
Installation
============
Yosys written in C++ (using features from C++11) and is tested on modern Linux.
It should compile fine on most UNIX systems with a C++11 compiler. The README
file contains useful information on building Yosys and its prerequisites.
Yosys is a large and feature-rich program with some dependencies. For this work,
we may deactivate other extra features such as TCL and ABC support in the
Makefile.
This Application Note is based on `Yosys GIT`_ `Rev. 082550f` from 2015-04-04.
.. _Yosys GIT: https://github.com/YosysHQ/yosys
.. _Rev. 082550f: https://github.com/YosysHQ/yosys/tree/082550f
Quick start
===========
We assume that the Verilog design is synthesizable and we also assume that the
design does not have multi-dimensional memories. As BTOR implicitly initializes
registers to zero value and memories stay uninitialized, we assume that the
Verilog design does not contain initial blocks. For more details about the BTOR
format, please refer to :cite:p:`btor`.
We provide a shell script ``verilog2btor.sh`` which can be used to convert a
Verilog design to BTOR. The script can be found in the ``backends/btor``
directory. The following example shows its usage:
.. code:: sh
verilog2btor.sh fsm.v fsm.btor test
The script ``verilog2btor.sh`` takes three parameters. In the above example, the
first parameter ``fsm.v`` is the input design, the second parameter ``fsm.btor``
is the file name of BTOR output, and the third parameter ``test`` is the name of
top module in the design.
To specify the properties (that need to be checked), we have two
options:
- We can use the Verilog ``assert`` statement in the procedural block or module
body of the Verilog design, as shown in :numref:`specifying_property_assert`.
This is the preferred option.
- We can use a single-bit output wire, whose name starts with ``safety``. The
value of this output wire needs to be driven low when the property is met,
i.e. the solver will try to find a model that makes the safety pin go high.
This is demonstrated in :numref:`specifying_property_output`.
.. code-block:: verilog
:caption: Specifying property in Verilog design with ``assert``
:name: specifying_property_assert
module test(input clk, input rst, output y);
reg [2:0] state;
always @(posedge clk) begin
if (rst || state == 3) begin
state <= 0;
end else begin
assert(state < 3);
state <= state + 1;
end
end
assign y = state[2];
assert property (y !== 1'b1);
endmodule
.. code-block:: verilog
:caption: Specifying property in Verilog design with output wire
:name: specifying_property_output
module test(input clk, input rst,
output y, output safety1);
reg [2:0] state;
always @(posedge clk) begin
if (rst || state == 3)
state <= 0;
else
state <= state + 1;
end
assign y = state[2];
assign safety1 = !(y !== 1'b1);
endmodule
We can run `Boolector`_ ``1.4.1`` [1]_ on the generated BTOR file:
.. _Boolector: http://fmv.jku.at/boolector/
.. code:: sh
$ boolector fsm.btor
unsat
We can also use `nuXmv`_, but on BTOR designs it does not support memories yet.
With the next release of nuXmv, we will be also able to verify designs with
memories.
.. _nuXmv: https://es-static.fbk.eu/tools/nuxmv/index.php
Detailed flow
=============
Yosys is able to synthesize Verilog designs up to the gate level. We are
interested in keeping registers and memories when synthesizing the design. For
this purpose, we describe a customized Yosys synthesis flow, that is also
provided by the ``verilog2btor.sh`` script. :numref:`btor_script_memory` shows
the Yosys commands that are executed by ``verilog2btor.sh``.
.. code-block:: yoscrypt
:caption: Synthesis Flow for BTOR with memories
:name: btor_script_memory
read_verilog -sv $1;
hierarchy -top $3; hierarchy -libdir $DIR;
hierarchy -check;
proc; opt;
opt_expr -mux_undef; opt;
rename -hide;;;
splice; opt;
memory_dff -wr_only; memory_collect;;
flatten;;
memory_unpack;
splitnets -driver;
setundef -zero -undriven;
opt;;;
write_btor $2;
Here is short description of what is happening in the script line by
line:
#. Reading the input file.
#. Setting the top module in the hierarchy and trying to read automatically the
files which are given as ``include`` in the file read in first line.
#. Checking the design hierarchy.
#. Converting processes to multiplexers (muxs) and flip-flops.
#. Removing undef signals from muxs.
#. Hiding all signal names that are not used as module ports.
#. Explicit type conversion, by introducing slice and concat cells in the
circuit.
#. Converting write memories to synchronous memories, and collecting the
memories to multi-port memories.
#. Flattening the design to get only one module.
#. Separating read and write memories.
#. Splitting the signals that are partially assigned
#. Setting undef to zero value.
#. Final optimization pass.
#. Writing BTOR file.
For detailed description of the commands mentioned above, please refer
to the Yosys documentation, or run ``yosys -h <command_name>``.
The script presented earlier can be easily modified to have a BTOR file that
does not contain memories. This is done by removing the line number 8 and 10,
and introduces a new command ``memory`` at line number 8.
:numref:`btor_script_without_memory` shows the modified Yosys script file:
.. code-block:: sh
:caption: Synthesis Flow for BTOR without memories
:name: btor_script_without_memory
read_verilog -sv $1;
hierarchy -top $3; hierarchy -libdir $DIR;
hierarchy -check;
proc; opt;
opt_expr -mux_undef; opt;
rename -hide;;;
splice; opt;
memory;;
flatten;;
splitnets -driver;
setundef -zero -undriven;
opt;;;
write_btor $2;
Example
=======
Here is an example Verilog design that we want to convert to BTOR:
.. code-block:: verilog
:caption: Example - Verilog Design
:name: example_verilog
module array(input clk);
reg [7:0] counter;
reg [7:0] mem [7:0];
always @(posedge clk) begin
counter <= counter + 8'd1;
mem[counter] <= counter;
end
assert property (!(counter > 8'd0) ||
mem[counter - 8'd1] == counter - 8'd1);
endmodule
The generated BTOR file that contain memories, using the script shown in
:numref:`btor_memory`:
.. code-block::
:caption: Example - Converted BTOR with memory
:name: btor_memory
1 var 1 clk
2 array 8 3
3 var 8 $auto$rename.cc:150:execute$20
4 const 8 00000001
5 sub 8 3 4
6 slice 3 5 2 0
7 read 8 2 6
8 slice 3 3 2 0
9 add 8 3 4
10 const 8 00000000
11 ugt 1 3 10
12 not 1 11
13 const 8 11111111
14 slice 1 13 0 0
15 one 1
16 eq 1 1 15
17 and 1 16 14
18 write 8 3 2 8 3
19 acond 8 3 17 18 2
20 anext 8 3 2 19
21 eq 1 7 5
22 or 1 12 21
23 const 1 1
24 one 1
25 eq 1 23 24
26 cond 1 25 22 24
27 root 1 -26
28 cond 8 1 9 3
29 next 8 3 28
And the BTOR file obtained by the script shown in
:numref:`btor_without_memory`, which expands the memory into individual
elements:
.. code-block::
:caption: Example - Converted BTOR with memory
:name: btor_without_memory
1 var 1 clk
2 var 8 mem[0]
3 var 8 $auto$rename.cc:150:execute$20
4 slice 3 3 2 0
5 slice 1 4 0 0
6 not 1 5
7 slice 1 4 1 1
8 not 1 7
9 slice 1 4 2 2
10 not 1 9
11 and 1 8 10
12 and 1 6 11
13 cond 8 12 3 2
14 cond 8 1 13 2
15 next 8 2 14
16 const 8 00000001
17 add 8 3 16
18 const 8 00000000
19 ugt 1 3 18
20 not 1 19
21 var 8 mem[2]
22 and 1 7 10
23 and 1 6 22
24 cond 8 23 3 21
25 cond 8 1 24 21
26 next 8 21 25
27 sub 8 3 16
...
54 cond 1 53 50 52
55 root 1 -54
...
77 cond 8 76 3 44
78 cond 8 1 77 44
79 next 8 44 78
Limitations
===========
BTOR does not support initialization of memories and registers, i.e. they are
implicitly initialized to value zero, so the initial block for memories need to
be removed when converting to BTOR. It should also be kept in consideration that
BTOR does not support the ``x`` or ``z`` values of Verilog.
Another thing to bear in mind is that Yosys will convert multi-dimensional
memories to one-dimensional memories and address decoders. Therefore
out-of-bounds memory accesses can yield unexpected results.
Conclusion
==========
Using the described flow, we can use Yosys to generate word-level verification
benchmarks with or without memories from Verilog designs.
.. [1]
Newer version of Boolector do not support sequential models.
Boolector 1.4.1 can be built with picosat-951. Newer versions of
picosat have an incompatible API.

42
docs/source/appendix/CHAPTER_Auxlibs.rst Normal file
View file

@ -0,0 +1,42 @@
Auxiliary libraries
===================
The Yosys source distribution contains some auxiliary libraries that are bundled
with Yosys.
SHA1
----
The files in ``libs/sha1/`` provide a public domain SHA1 implementation written
by Steve Reid, Bruce Guenter, and Volker Grabsch. It is used for generating
unique names when specializing parameterized modules.
BigInt
------
The files in ``libs/bigint/`` provide a library for performing arithmetic with
arbitrary length integers. It is written by Matt McCutchen.
The BigInt library is used for evaluating constant expressions, e.g. using the
ConstEval class provided in kernel/consteval.h.
See also: http://mattmccutchen.net/bigint/
.. _sec:SubCircuit:
SubCircuit
----------
The files in ``libs/subcircuit`` provide a library for solving the subcircuit
isomorphism problem. It is written by C. Wolf and based on the Ullmann Subgraph
Isomorphism Algorithm :cite:p:`UllmannSubgraphIsomorphism`. It is used by the
extract pass (see :doc:`../cmd/extract`).
ezSAT
-----
The files in ``libs/ezsat`` provide a library for simplifying generating CNF
formulas for SAT solvers. It also contains bindings of MiniSAT. The ezSAT
library is written by C. Wolf. It is used by the sat pass (see
:doc:`../cmd/sat`).

29
docs/source/appendix/CHAPTER_Auxprogs.rst Normal file
View file

@ -0,0 +1,29 @@
Auxiliary programs
==================
Besides the main yosys executable, the Yosys distribution contains a set of
additional helper programs.
yosys-config
------------
The yosys-config tool (an auto-generated shell-script) can be used to query
compiler options and other information needed for building loadable modules for
Yosys. See Sec. \ :numref:`chapter:prog` for details.
.. _sec:filterlib:
yosys-filterlib
---------------
The yosys-filterlib tool is a small utility that can be used to strip or extract
information from a Liberty file. See :numref:`Sec. %s <sec:techmap_extern>` for
details.
yosys-abc
---------
This is a fork of ABC with a small set of custom modifications that have not yet
been accepted upstream. Not all versions of Yosys work with all versions of ABC.
So Yosys comes with its own yosys-abc to avoid compatibility issues between the
two.

410
docs/source/appendix/CHAPTER_StateOfTheArt.rst Normal file
View file

@ -0,0 +1,410 @@
.. _chapter:sota:
Evaluation of other OSS Verilog Synthesis Tools
===============================================
In this appendix [1]_ the existing FOSS Verilog synthesis tools [2]_ are
evaluated. Extremely limited or application specific tools (e.g. pure
Verilog Netlist parsers) as well as Verilog simulators are not included.
These existing solutions are tested using a set of representative
Verilog code snippets. It is shown that no existing FOSS tool implements
even close to a sufficient subset of Verilog to be usable as synthesis
tool for a wide range existing Verilog code.
The packages evaluated are:
- Icarus Verilog [3]_
- Verilog-to-Routing (VTR) / Odin-II
:cite:p:`vtr2012}`:raw-latex:`\cite{Odin`
- HDL Analyzer and Netlist Architect (HANA)
- Verilog front-end to VIS (vl2mv) :cite:p:`Cheng93vl2mv:a`
In each of the following sections Verilog modules that test a certain
Verilog language feature are presented and the support for these
features is tested in all the tools mentioned above. It is evaluated
whether the tools under test successfully generate netlists for the
Verilog input and whether these netlists match the simulation behavior
of the designs using testbenches.
All test cases are verified to be synthesizeable using Xilinx XST from
the Xilinx WebPACK suite.
Trivial features such as support for simple structural Verilog are not
explicitly tested.
Vl2mv and Odin-II generate output in the BLIF (Berkeley Logic
Interchange Format) and BLIF-MV (an extended version of BLIF) formats
respectively. ABC is used to convert this output to Verilog for
verification using testbenches.
Icarus Verilog generates EDIF (Electronic Design Interchange Format)
output utilizing LPM (Library of Parameterized Modules) cells. The EDIF
files are converted to Verilog using edif2ngd and netgen from Xilinx
WebPACK. A hand-written implementation of the LPM cells utilized by the
generated netlists is used for verification.
Following these functional tests, a quick analysis of the extensibility
of the tools under test is provided in a separate section.
The last section of this chapter finally concludes these series of
evaluations with a summary of the results.
.. code:: verilog
:number-lines:
module uut_always01(clock,
reset, count);
input clock, reset;
output [3:0] count;
reg [3:0] count;
always @(posedge clock)
count <= reset ?
0 : count + 1;
endmodule
.. code:: verilog
module uut_always02(clock,
reset, count);
input clock, reset;
output [3:0] count;
reg [3:0] count;
always @(posedge clock) begin
count <= count + 1;
if (reset)
count <= 0;
end
endmodule
[fig:StateOfTheArt_always12]
.. code:: verilog
:number-lines:
module uut_always03(clock, in1, in2, in3, in4, in5, in6, in7,
out1, out2, out3);
input clock, in1, in2, in3, in4, in5, in6, in7;
output out1, out2, out3;
reg out1, out2, out3;
always @(posedge clock) begin
out1 = in1;
if (in2)
out1 = !out1;
out2 <= out1;
if (in3)
out2 <= out2;
if (in4)
if (in5)
out3 <= in6;
else
out3 <= in7;
out1 = out1 ^ out2;
end
endmodule
[fig:StateOfTheArt_always3]
.. _sec:blocking_nonblocking:
Always blocks and blocking vs. nonblocking assignments
------------------------------------------------------
The "always"-block is one of the most fundamental non-trivial Verilog
language features. It can be used to model a combinatorial path (with
optional registers on the outputs) in a way that mimics a regular
programming language.
Within an always block, if- and case-statements can be used to model
multiplexers. Blocking assignments (:math:`=`) and nonblocking
assignments (:math:`<=`) are used to populate the leaf-nodes of these
multiplexer trees. Unassigned leaf-nodes default to feedback paths that
cause the output register to hold the previous value. More advanced
synthesis tools often convert these feedback paths to register enable
signals or even generate circuits with clock gating.
Registers assigned with nonblocking assignments (:math:`<=`) behave
differently from variables in regular programming languages: In a
simulation they are not updated immediately after being assigned.
Instead the right-hand sides are evaluated and the results stored in
temporary memory locations. After all pending updates have been prepared
in this way they are executed, thus yielding semi-parallel execution of
all nonblocking assignments.
For synthesis this means that every occurrence of that register in an
expression addresses the output port of the corresponding register
regardless of the question whether the register has been assigned a new
value in an earlier command in the same always block. Therefore with
nonblocking assignments the order of the assignments has no effect on
the resulting circuit as long as the left-hand sides of the assignments
are unique.
The three example codes in
:numref:`Fig. %s <fig:StateOfTheArt_always12>`
and :numref:`Fig. %s <fig:StateOfTheArt_always3>`
use all these features and can thus be used to test the synthesis tools
capabilities to synthesize always blocks correctly.
The first example is only using the most fundamental Verilog features.
All tools under test were able to successfully synthesize this design.
.. code:: verilog
:number-lines:
module uut_arrays01(clock, we, addr, wr_data, rd_data);
input clock, we;
input [3:0] addr, wr_data;
output [3:0] rd_data;
reg [3:0] rd_data;
reg [3:0] memory [15:0];
always @(posedge clock) begin
if (we)
memory[addr] <= wr_data;
rd_data <= memory[addr];
end
endmodule
[fig:StateOfTheArt_arrays]
The 2nd example is functionally identical to the 1st one but is using an
if-statement inside the always block. Odin-II fails to synthesize it and
instead produces the following error message:
::
ERROR: (File: always02.v) (Line number: 13)
You've defined the driver "count~0" twice
Vl2mv does not produce an error message but outputs an invalid synthesis
result that is not using the reset input at all.
Icarus Verilog also doesn't produce an error message but generates an
invalid output for this 2nd example. The code generated by Icarus
Verilog only implements the reset path for the count register,
effectively setting the output to constant 0.
So of all tools under test only HANA was able to create correct
synthesis results for the 2nd example.
The 3rd example is using blocking and nonblocking assignments and many
if statements. Odin also fails to synthesize this example:
::
ERROR: (File: always03.v) (Line number: 8)
ODIN doesn't handle blocking statements in Sequential blocks
HANA, Icarus Verilog and vl2mv create invalid synthesis results for the
3rd example.
So unfortunately none of the tools under test provide a complete and
correct implementation of blocking and nonblocking assignments.
Arrays for memory modelling
---------------------------
Verilog arrays are part of the synthesizeable subset of Verilog and are
commonly used to model addressable memory. The Verilog code in
:numref:`Fig. %s <fig:StateOfTheArt_arrays>`
demonstrates this by implementing a single port memory.
For this design HANA, vl2m and ODIN-II generate error messages
indicating that arrays are not supported.
.. code:: verilog
:number-lines:
module uut_forgen01(a, y);
input [4:0] a;
output y;
integer i, j;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
[fig:StateOfTheArt_for]
Icarus Verilog produces an invalid output that is using the address only
for reads. Instead of using the address input for writes, the generated
design simply loads the data to all memory locations whenever the
write-enable input is active, effectively turning the design into a
single 4-bit D-Flip-Flop with enable input.
As all tools under test already fail this simple test, there is nothing
to gain by continuing tests on this aspect of Verilog synthesis such as
synthesis of dual port memories, correct handling of write collisions,
and so forth.
.. code:: verilog
:number-lines:
module uut_forgen02(a, b, cin, y, cout);
parameter WIDTH = 8;
input [WIDTH-1:0] a, b;
input cin;
output [WIDTH-1:0] y;
output cout;
genvar i;
wire [WIDTH-1:0] carry;
generate
for (i = 0; i < WIDTH; i=i+1) begin:adder
wire [2:0] D;
assign D[1:0] = { a[i], b[i] };
if (i == 0) begin:chain
assign D[2] = cin;
end else begin:chain
assign D[2] = carry[i-1];
end
assign y[i] = ^D;
assign carry[i] = &D[1:0] | (^D[1:0] & D[2]);
end
endgenerate
assign cout = carry[WIDTH-1];
endmodule
[fig:StateOfTheArt_gen]
For-loops and generate blocks
-----------------------------
For-loops and generate blocks are more advanced Verilog features. These
features allow the circuit designer to add program code to her design
that is evaluated during synthesis to generate (parts of) the circuits
description; something that could only be done using a code generator
otherwise.
For-loops are only allowed in synthesizeable Verilog if they can be
completely unrolled. Then they can be a powerful tool to generate array
logic or static lookup tables. The code in
:numref:`Fig. %s <fig:StateOfTheArt_for>` generates a
circuit that tests a 5 bit value for being a prime number using a static
lookup table.
Generate blocks can be used to model array logic in complex parametric
designs. The code in
:numref:`Fig. %s <fig:StateOfTheArt_gen>` implements a
ripple-carry adder with parametric width from simple assign-statements
and logic operations using a Verilog generate block.
All tools under test failed to synthesize both test cases. HANA creates
invalid output in both cases. Icarus Verilog creates invalid output for
the first test and fails with an error for the second case. The other
two tools fail with error messages for both tests.
Extensibility
-------------
This section briefly discusses the extensibility of the tools under test
and their internal data- and control-flow. As all tools under test
already failed to synthesize simple Verilog always-blocks correctly, not
much resources have been spent on evaluating the extensibility of these
tools and therefore only a very brief discussion of the topic is
provided here.
HANA synthesizes for a built-in library of standard cells using two
passes over an AST representation of the Verilog input. This approach
executes fast but limits the extensibility as everything happens in only
two comparable complex AST walks and there is no universal intermediate
representation that is flexible enough to be used in arbitrary
optimizations.
Odin-II and vl2m are both front ends to existing synthesis flows. As
such they only try to quickly convert the Verilog input into the
internal representation of their respective flows (BLIF). So
extensibility is less of an issue here as potential extensions would
likely be implemented in other components of the flow.
Icarus Verilog is clearly designed to be a simulation tool rather than a
synthesis tool. The synthesis part of Icarus Verilog is an ad-hoc add-on
to Icarus Verilog that aims at converting an internal representation
that is meant for generation of a virtual machine based simulation code
to netlists.
Summary and Outlook
-------------------
Table \ :numref:`tab:StateOfTheArt_sum` summarizes
the tests performed. Clearly none of the tools under test make a serious
attempt at providing a feature-complete implementation of Verilog. It
can be argued that Odin-II performed best in the test as it never
generated incorrect code but instead produced error messages indicating
that unsupported Verilog features where used in the Verilog input.
In conclusion, to the best knowledge of the author, there is no FOSS
Verilog synthesis tool other than Yosys that is anywhere near feature
completeness and therefore there is no other candidate for a generic
Verilog front end and/or synthesis framework to be used as a basis for
custom synthesis tools.
Yosys could also replace vl2m and/or Odin-II in their respective flows
or function as a pre-compiler that can translate full-featured Verilog
code to the simple subset of Verilog that is understood by vl2m and
Odin-II.
Yosys is designed for extensibility. It can be used as-is to synthesize
Verilog code to netlists, but its main purpose is to be used as basis
for custom tools. Yosys is structured in a language dependent Verilog
front end and language independent synthesis code (which is in itself
structured in independent passes). This architecture will simplify
implementing additional HDL front ends and/or additional synthesis
passes.
Chapter \ :numref:`<CHAPTER_eval>` contains a more detailed
evaluation of Yosys using real-world designs that are far out of reach
for any of the other tools discussed in this appendix.
…passed 2em …produced error 2em :math:`\skull` …incorrect output
[tab:StateOfTheArt_sum]
.. [1]
This appendix is an updated version of an unpublished student
research paper. :cite:p:`VerilogFossEval`
.. [2]
To the author's best knowledge, all relevant tools that existed at
the time of this writing are included. But as there is no formal
channel through which such tools are published it is hard to give any
guarantees in that matter.
.. [3]
Icarus Verilog is mainly a simulation tool but also supported
synthesis up to version 0.8. Therefore version 0.8.7 is used for this
evaluation.)

298
docs/source/appendix/CHAPTER_TextRtlil.rst Normal file
View file

@ -0,0 +1,298 @@
.. _chapter:textrtlil:
RTLIL text representation
=========================
This appendix documents the text representation of RTLIL in extended Backus-Naur
form (EBNF).
The grammar is not meant to represent semantic limitations. That is, the grammar
is "permissive", and later stages of processing perform more rigorous checks.
The grammar is also not meant to represent the exact grammar used in the RTLIL
frontend, since that grammar is specific to processing by lex and yacc, is even
more permissive, and is somewhat less understandable than simple EBNF notation.
Finally, note that all statements (rules ending in ``-stmt``) terminate in an
end-of-line. Because of this, a statement cannot be broken into multiple lines.
Lexical elements
----------------
Characters
~~~~~~~~~~
An RTLIL file is a stream of bytes. Strictly speaking, a "character" in an RTLIL
file is a single byte. The lexer treats multi-byte encoded characters as
consecutive single-byte characters. While other encodings *may* work, UTF-8 is
known to be safe to use. Byte order marks at the beginning of the file will
cause an error.
ASCII spaces (32) and tabs (9) separate lexer tokens.
A ``nonws`` character, used in identifiers, is any character whose encoding
consists solely of bytes above ASCII space (32).
An ``eol`` is one or more consecutive ASCII newlines (10) and carriage returns
(13).
Identifiers
~~~~~~~~~~~
There are two types of identifiers in RTLIL:
- Publically visible identifiers
- Auto-generated identifiers
.. code:: BNF
<id> ::= <public-id> | <autogen-id>
<public-id> ::= \ <nonws>+
<autogen-id> ::= $ <nonws>+
Values
~~~~~~
A *value* consists of a width in bits and a bit representation, most
significant bit first. Bits may be any of:
- ``0``: A logic zero value
- ``1``: A logic one value
- ``x``: An unknown logic value (or don't care in case patterns)
- ``z``: A high-impedance value (or don't care in case patterns)
- ``m``: A marked bit (internal use only)
- ``-``: A don't care value
An *integer* is simply a signed integer value in decimal format. **Warning:**
Integer constants are limited to 32 bits. That is, they may only be in the range
:math:`[-2147483648, 2147483648)`. Integers outside this range will result in an
error.
.. code:: BNF
<value> ::= <decimal-digit>+ ' <binary-digit>*
<decimal-digit> ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
<binary-digit> ::= 0 | 1 | x | z | m | -
<integer> ::= -? <decimal-digit>+
Strings
~~~~~~~
A string is a series of characters delimited by double-quote characters. Within
a string, any character except ASCII NUL (0) may be used. In addition, certain
escapes can be used:
- ``\n``: A newline
- ``\t``: A tab
- ``\ooo``: A character specified as a one, two, or three digit octal value
All other characters may be escaped by a backslash, and become the following
character. Thus:
- ``\\``: A backslash
- ``\"``: A double-quote
- ``\r``: An 'r' character
Comments
~~~~~~~~
A comment starts with a ``#`` character and proceeds to the end of the line. All
comments are ignored.
File
----
A file consists of an optional autoindex statement followed by zero or more
modules.
.. code:: BNF
<file> ::= <autoidx-stmt>? <module>*
Autoindex statements
~~~~~~~~~~~~~~~~~~~~
The autoindex statement sets the global autoindex value used by Yosys when it
needs to generate a unique name, e.g. ``flattenN``. The N part is filled with
the value of the global autoindex value, which is subsequently incremented. This
global has to be dumped into RTLIL, otherwise e.g. dumping and running a pass
would have different properties than just running a pass on a warm design.
.. code:: BNF
<autoidx-stmt> ::= autoidx <integer> <eol>
Modules
~~~~~~~
Declares a module, with zero or more attributes, consisting of zero or more
wires, memories, cells, processes, and connections.
.. code:: BNF
<module> ::= <attr-stmt>* <module-stmt> <module-body> <module-end-stmt>
<module-stmt> ::= module <id> <eol>
<module-body> ::= (<param-stmt>
| <wire>
| <memory>
| <cell>
| <process>)*
<param-stmt> ::= parameter <id> <constant>? <eol>
<constant> ::= <value> | <integer> | <string>
<module-end-stmt> ::= end <eol>
Attribute statements
~~~~~~~~~~~~~~~~~~~~
Declares an attribute with the given identifier and value.
.. code:: BNF
<attr-stmt> ::= attribute <id> <constant> <eol>
Signal specifications
~~~~~~~~~~~~~~~~~~~~~
A signal is anything that can be applied to a cell port, i.e. a constant value,
all bits or a selection of bits from a wire, or concatenations of those.
**Warning:** When an integer constant is a sigspec, it is always 32 bits wide,
2's complement. For example, a constant of :math:`-1` is the same as
``32'11111111111111111111111111111111``, while a constant of :math:`1` is the
same as ``32'1``.
See :numref:`Sec. %s <sec:rtlil_sigspec>` for an overview of signal
specifications.
.. code:: BNF
<sigspec> ::= <constant>
| <wire-id>
| <sigspec> [ <integer> (:<integer>)? ]
| { <sigspec>* }
Connections
~~~~~~~~~~~
Declares a connection between the given signals.
.. code:: BNF
<conn-stmt> ::= connect <sigspec> <sigspec> <eol>
Wires
~~~~~
Declares a wire, with zero or more attributes, with the given identifier and
options in the enclosing module.
See :numref:`Sec. %s <sec:rtlil_cell_wire>` for an overview of wires.
.. code:: BNF
<wire> ::= <attr-stmt>* <wire-stmt>
<wire-stmt> ::= wire <wire-option>* <wire-id> <eol>
<wire-id> ::= <id>
<wire-option> ::= width <integer>
| offset <integer>
| input <integer>
| output <integer>
| inout <integer>
| upto
| signed
Memories
~~~~~~~~
Declares a memory, with zero or more attributes, with the given identifier and
options in the enclosing module.
See :numref:`Sec. %s <sec:rtlil_memory>` for an overview of memory cells, and
:numref:`Sec. %s <sec:memcells>` for details about memory cell types.
.. code:: BNF
<memory> ::= <attr-stmt>* <memory-stmt>
<memory-stmt> ::= memory <memory-option>* <id> <eol>
<memory-option> ::= width <integer>
| size <integer>
| offset <integer>
Cells
~~~~~
Declares a cell, with zero or more attributes, with the given identifier and
type in the enclosing module.
Cells perform functions on input signals. See :numref:`Chap. %s
<chapter:celllib>` for a detailed list of cell types.
.. code:: BNF
<cell> ::= <attr-stmt>* <cell-stmt> <cell-body-stmt>* <cell-end-stmt>
<cell-stmt> ::= cell <cell-type> <cell-id> <eol>
<cell-id> ::= <id>
<cell-type> ::= <id>
<cell-body-stmt> ::= parameter (signed | real)? <id> <constant> <eol>
| connect <id> <sigspec> <eol>
<cell-end-stmt> ::= end <eol>
Processes
~~~~~~~~~
Declares a process, with zero or more attributes, with the given identifier in
the enclosing module. The body of a process consists of zero or more
assignments, exactly one switch, and zero or more syncs.
See :numref:`Sec. %s <sec:rtlil_process>` for an overview of processes.
.. code:: BNF
<process> ::= <attr-stmt>* <proc-stmt> <process-body> <proc-end-stmt>
<proc-stmt> ::= process <id> <eol>
<process-body> ::= <assign-stmt>* <switch>? <assign-stmt>* <sync>*
<assign-stmt> ::= assign <dest-sigspec> <src-sigspec> <eol>
<dest-sigspec> ::= <sigspec>
<src-sigspec> ::= <sigspec>
<proc-end-stmt> ::= end <eol>
Switches
~~~~~~~~
Switches test a signal for equality against a list of cases. Each case specifies
a comma-separated list of signals to check against. If there are no signals in
the list, then the case is the default case. The body of a case consists of zero
or more switches and assignments. Both switches and cases may have zero or more
attributes.
.. code:: BNF
<switch> ::= <switch-stmt> <case>* <switch-end-stmt>
<switch-stmt> := <attr-stmt>* switch <sigspec> <eol>
<case> ::= <attr-stmt>* <case-stmt> <case-body>
<case-stmt> ::= case <compare>? <eol>
<compare> ::= <sigspec> (, <sigspec>)*
<case-body> ::= (<switch> | <assign-stmt>)*
<switch-end-stmt> ::= end <eol>
Syncs
~~~~~
Syncs update signals with other signals when an event happens. Such an event may
be:
- An edge or level on a signal
- Global clock ticks
- Initialization
- Always
.. code:: BNF
<sync> ::= <sync-stmt> <update-stmt>*
<sync-stmt> ::= sync <sync-type> <sigspec> <eol>
| sync global <eol>
| sync init <eol>
| sync always <eol>
<sync-type> ::= low | high | posedge | negedge | edge
<update-stmt> ::= update <dest-sigspec> <src-sigspec> <eol>