diff --git a/docs/source/_downloads/APPNOTE_010_Verilog_to_BLIF.pdf b/docs/source/_downloads/APPNOTE_010_Verilog_to_BLIF.pdf new file mode 100644 index 000000000..91fc1aac8 Binary files /dev/null and b/docs/source/_downloads/APPNOTE_010_Verilog_to_BLIF.pdf differ diff --git a/docs/source/_downloads/APPNOTE_012_Verilog_to_BTOR.pdf b/docs/source/_downloads/APPNOTE_012_Verilog_to_BTOR.pdf new file mode 100644 index 000000000..f3ffd6f30 Binary files /dev/null and b/docs/source/_downloads/APPNOTE_012_Verilog_to_BTOR.pdf differ diff --git a/docs/source/appendix.rst b/docs/source/appendix.rst index 04ee2945c..0b0a2d15b 100644 --- a/docs/source/appendix.rst +++ b/docs/source/appendix.rst @@ -9,9 +9,6 @@ Appendix appendix/auxlibs appendix/auxprogs - appendix/APPNOTE_010_Verilog_to_BLIF.rst - appendix/APPNOTE_012_Verilog_to_BTOR.rst - bib .. toctree:: diff --git a/docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst b/docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst index d8f8fec46..cc658f03f 100644 --- a/docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst +++ b/docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst @@ -1,333 +1,363 @@ +:orphan: + ==================================== 010: Converting Verilog to BLIF page ==================================== -Installation -============ +Abstract +======== -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. +Verilog-2005 is a powerful Hardware Description Language (HDL) that can be used +to easily create complex designs from small HDL code. It is the preferred method +of design entry for many designers. -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. +The Berkeley Logic Interchange Format (BLIF) is a simple file format for +exchanging sequential logic between programs. It is easy to generate and easy to +parse and is therefore the preferred method of design entry for many authors of +logic synthesis tools. -.. _Yosys GIT: https://github.com/YosysHQ/yosys +Yosys is a feature-rich Open-Source Verilog synthesis tool that can be used to +bridge the gap between the two file formats. It implements most of Verilog-2005 +and thus can be used to import modern behavioral Verilog designs into BLIF-based +design flows without dependencies on proprietary synthesis tools. -.. _Rev. e216e0e: https://github.com/YosysHQ/yosys/tree/e216e0e +The scope of Yosys goes of course far beyond Verilog logic synthesis. But it is +a useful and important feature and this Application Note will focus on this +aspect of Yosys. -.. _yosys-bigsim: https://github.com/YosysHQ/yosys-bigsim +Download +======== -Getting started -=============== +This document was originally published in April 2015: +:download:`Converting Verilog to BLIF PDF` -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 +.. + Installation + ============ -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. + 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. -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. + 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. -Using a synthesis script -======================== + .. _Yosys GIT: https://github.com/YosysHQ/yosys -With a script file we have better control over Yosys. The following -script file replicates what the command from the last section did: + .. _Rev. e216e0e: https://github.com/YosysHQ/yosys/tree/e216e0e -.. 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 :cmd:ref:`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 - #include - - #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. + .. _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 :cmd:ref:`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 + #include + + #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_012_Verilog_to_BTOR.rst b/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst index adb551494..1874b0148 100644 --- a/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst +++ b/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst @@ -1,333 +1,353 @@ +:orphan: + ==================================== 012: Converting Verilog to BTOR page ==================================== -Installation -============ +Abstract +======== -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. +Verilog-2005 is a powerful Hardware Description Language (HDL) that can be used +to easily create complex designs from small HDL code. BTOR is a bit-precise +word-level format for model checking. It is a simple format and easy to parse. +It allows to model the model checking problem over the theory of bit-vectors +with one-dimensional arrays, thus enabling to model Verilog designs with +registers and memories. Yosys is an Open-Source Verilog synthesis tool that can +be used to convert Verilog designs with simple assertions to BTOR format. -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. +Download +======== -This Application Note is based on `Yosys GIT`_ `Rev. 082550f` from 2015-04-04. +This document was originally published in November 2013: +:download:`Converting Verilog to BTOR PDF` -.. _Yosys GIT: https://github.com/YosysHQ/yosys +.. + Installation + ============ -.. _Rev. 082550f: https://github.com/YosysHQ/yosys/tree/082550f + 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. -Quick start -=========== + 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. -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`. + This Application Note is based on `Yosys GIT`_ `Rev. 082550f` from 2015-04-04. -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: + .. _Yosys GIT: https://github.com/YosysHQ/yosys -.. code:: sh + .. _Rev. 082550f: https://github.com/YosysHQ/yosys/tree/082550f - verilog2btor.sh fsm.v fsm.btor test + Quick start + =========== -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. + 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`. -To specify the properties (that need to be checked), we have two -options: + 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: -- 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. + .. code:: sh -- 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`. + verilog2btor.sh fsm.v fsm.btor test -.. code-block:: verilog - :caption: Specifying property in Verilog design with ``assert`` - :name: specifying_property_assert + 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. - module test(input clk, input rst, output y); + To specify the properties (that need to be checked), we have two + options: - reg [2:0] state; + - 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. - always @(posedge clk) begin - if (rst || state == 3) begin - state <= 0; - end else begin - assert(state < 3); - state <= state + 1; - end - end + - 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`. - assign y = state[2]; + .. code-block:: verilog + :caption: Specifying property in Verilog design with ``assert`` + :name: specifying_property_assert - assert property (y !== 1'b1); + module test(input clk, input rst, output y); - endmodule + reg [2:0] state; -.. code-block:: verilog - :caption: Specifying property in Verilog design with output wire - :name: specifying_property_output + always @(posedge clk) begin + if (rst || state == 3) begin + state <= 0; + end else begin + assert(state < 3); + state <= state + 1; + end + end - module test(input clk, input rst, - output y, output safety1); + assign y = state[2]; - reg [2:0] state; + assert property (y !== 1'b1); - always @(posedge clk) begin - if (rst || state == 3) - state <= 0; - else - state <= state + 1; - end + endmodule - assign y = state[2]; + .. code-block:: verilog + :caption: Specifying property in Verilog design with output wire + :name: specifying_property_output - assign safety1 = !(y !== 1'b1); + module test(input clk, input rst, + output y, output safety1); - endmodule + reg [2:0] state; -We can run `Boolector`_ ``1.4.1`` [1]_ on the generated BTOR file: + always @(posedge clk) begin + if (rst || state == 3) + state <= 0; + else + state <= state + 1; + end -.. _Boolector: http://fmv.jku.at/boolector/ + assign y = state[2]; -.. code:: sh + assign safety1 = !(y !== 1'b1); - $ boolector fsm.btor - unsat + endmodule -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. + We can run `Boolector`_ ``1.4.1`` [1]_ on the generated BTOR file: -.. _nuXmv: https://es-static.fbk.eu/tools/nuxmv/index.php + .. _Boolector: http://fmv.jku.at/boolector/ -Detailed flow -============= + .. code:: sh -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``. + $ boolector fsm.btor + unsat -.. code-block:: yoscrypt - :caption: Synthesis Flow for BTOR with memories - :name: btor_script_memory + 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. - 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; + .. _nuXmv: https://es-static.fbk.eu/tools/nuxmv/index.php -Here is short description of what is happening in the script line by -line: + Detailed flow + ============= -#. Reading the input file. + 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``. -#. 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. + .. code-block:: yoscrypt + :caption: Synthesis Flow for BTOR with memories + :name: btor_script_memory -#. Checking the design hierarchy. + 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; -#. Converting processes to multiplexers (muxs) and flip-flops. + Here is short description of what is happening in the script line by + line: -#. Removing undef signals from muxs. + #. Reading the input file. -#. Hiding all signal names that are not used as module ports. + #. 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. -#. Explicit type conversion, by introducing slice and concat cells in the - circuit. + #. Checking the design hierarchy. -#. Converting write memories to synchronous memories, and collecting the - memories to multi-port memories. + #. Converting processes to multiplexers (muxs) and flip-flops. -#. Flattening the design to get only one module. + #. Removing undef signals from muxs. -#. Separating read and write memories. + #. Hiding all signal names that are not used as module ports. -#. Splitting the signals that are partially assigned + #. Explicit type conversion, by introducing slice and concat cells in the + circuit. -#. Setting undef to zero value. + #. Converting write memories to synchronous memories, and collecting the + memories to multi-port memories. -#. Final optimization pass. + #. Flattening the design to get only one module. -#. Writing BTOR file. + #. Separating read and write memories. -For detailed description of the commands mentioned above, please refer -to the Yosys documentation, or run ``yosys -h ``. - -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 :cmd:ref:`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. + #. 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 ``. + + 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 :cmd:ref:`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.