diff options
Diffstat (limited to 'docs/source/appendix')
| -rw-r--r-- | docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst | 336 | ||||
| -rw-r--r-- | docs/source/appendix/APPNOTE_011_Design_Investigation.rst | 965 | ||||
| -rw-r--r-- | docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst | 333 | ||||
| -rw-r--r-- | docs/source/appendix/CHAPTER_Auxlibs.rst | 42 | ||||
| -rw-r--r-- | docs/source/appendix/CHAPTER_Auxprogs.rst | 29 | ||||
| -rw-r--r-- | docs/source/appendix/CHAPTER_StateOfTheArt.rst | 410 | ||||
| -rw-r--r-- | docs/source/appendix/CHAPTER_TextRtlil.rst | 298 |
7 files changed, 2413 insertions, 0 deletions
diff --git a/docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst b/docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst new file mode 100644 index 000000000..a48401dcc --- /dev/null +++ b/docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst @@ -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. diff --git a/docs/source/appendix/APPNOTE_011_Design_Investigation.rst b/docs/source/appendix/APPNOTE_011_Design_Investigation.rst new file mode 100644 index 000000000..44819e283 --- /dev/null +++ b/docs/source/appendix/APPNOTE_011_Design_Investigation.rst @@ -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:: ../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:: ../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:: ../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:: ../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:: ../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. diff --git a/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst b/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst new file mode 100644 index 000000000..e9e44d1cd --- /dev/null +++ b/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst @@ -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. diff --git a/docs/source/appendix/CHAPTER_Auxlibs.rst b/docs/source/appendix/CHAPTER_Auxlibs.rst new file mode 100644 index 000000000..361f00e02 --- /dev/null +++ b/docs/source/appendix/CHAPTER_Auxlibs.rst @@ -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`). + diff --git a/docs/source/appendix/CHAPTER_Auxprogs.rst b/docs/source/appendix/CHAPTER_Auxprogs.rst new file mode 100644 index 000000000..e4f6f62cf --- /dev/null +++ b/docs/source/appendix/CHAPTER_Auxprogs.rst @@ -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. diff --git a/docs/source/appendix/CHAPTER_StateOfTheArt.rst b/docs/source/appendix/CHAPTER_StateOfTheArt.rst new file mode 100644 index 000000000..894d0fbbe --- /dev/null +++ b/docs/source/appendix/CHAPTER_StateOfTheArt.rst @@ -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.) diff --git a/docs/source/appendix/CHAPTER_TextRtlil.rst b/docs/source/appendix/CHAPTER_TextRtlil.rst new file mode 100644 index 000000000..dc3d72230 --- /dev/null +++ b/docs/source/appendix/CHAPTER_TextRtlil.rst @@ -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> |