mirror of https://github.com/YosysHQ/yosys.git
Replace 010 and 012 with pdf
Comment out the body text and instead include just the abstract and a download link. Also orphan the pages so they aren't accessible except by direct link, or via search.
This commit is contained in:
Krystine Sherwin
parent
17749ce688
commit
abd92225a3
Binary file not shown.
Binary file not shown.
|
|
@ -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::
|
||||
|
|
|
|||
|
|
@ -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</_downloads/APPNOTE_012_Verilog_to_BTOR.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 <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.
|
||||
.. _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 <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.
|
||||
|
|
|
|||
|
|
@ -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</_downloads/APPNOTE_012_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 <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 :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 <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 :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.
|
||||
|
|
|
|||
Loading…
Reference in New Issue