mirror of https://github.com/YosysHQ/yosys.git
136 lines
6.9 KiB
ReStructuredText
136 lines
6.9 KiB
ReStructuredText
Compiling with Verific library
|
|
==============================
|
|
|
|
The easiest way to get Yosys with Verific support is to `contact YosysHQ`_ for a
|
|
`Tabby CAD Suite`_ evaluation license and download link. The TabbyCAD Suite
|
|
includes additional patches and a custom extensions library in order to get the
|
|
most out of the Verific parser when using Yosys.
|
|
|
|
If you already have a license for the Verific parser, in either source or binary
|
|
form, you may be able to compile Yosys with partial Verific support yourself.
|
|
|
|
.. _contact YosysHQ : https://www.yosyshq.com/contact
|
|
.. _Tabby CAD Suite: https://www.yosyshq.com/tabby-cad-datasheet
|
|
|
|
The Yosys-Verific patch
|
|
-----------------------
|
|
|
|
YosysHQ maintains and develops a patch for Verific in order to better integrate
|
|
with Yosys and to provide features required by some of the formal verification
|
|
front-end tools. Synthesis from RTL may be possible without this patch, however
|
|
we are unable to provide support for any Yosys+Verific builds without it. To
|
|
license this patch for your own Yosys builds, `contact YosysHQ`_.
|
|
|
|
.. warning::
|
|
|
|
Some of the formal verification front-end tools may not be fully supported
|
|
without the full TabbyCAD suite. If you are wanting to use these tools,
|
|
including SBY, make sure to ask us if the Yosys-Verific patch is right for
|
|
you.
|
|
|
|
Compile options
|
|
---------------
|
|
|
|
To enable Verific support ``ENABLE_VERIFIC`` has to be set to ``1`` and
|
|
``VERIFIC_DIR`` needs to point to the location where the library is located.
|
|
|
|
============== ========================== ===============================
|
|
Parameter Default Description
|
|
============== ========================== ===============================
|
|
ENABLE_VERIFIC 0 Enable compilation with Verific
|
|
VERIFIC_DIR /usr/local/src/verific_lib Library and headers location
|
|
============== ========================== ===============================
|
|
|
|
Since there are multiple Verific library builds and they can have different
|
|
features, there are compile options to select them.
|
|
|
|
================================= ======= ===================================
|
|
Parameter Default Description
|
|
================================= ======= ===================================
|
|
ENABLE_VERIFIC_SYSTEMVERILOG 1 SystemVerilog support
|
|
ENABLE_VERIFIC_VHDL 1 VHDL support
|
|
ENABLE_VERIFIC_HIER_TREE 1 Hierarchy tree support
|
|
ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 YosysHQ specific extensions support
|
|
ENABLE_VERIFIC_EDIF 0 EDIF support
|
|
ENABLE_VERIFIC_LIBERTY 0 Liberty file support
|
|
================================= ======= ===================================
|
|
|
|
To find the compile options used for a given Yosys build, call ``yosys-config
|
|
--cxxflags``. This documentation was built with the following compile options:
|
|
|
|
.. literalinclude:: /generated/yosys-config
|
|
:start-at: --cxxflags
|
|
:end-before: --linkflags
|
|
|
|
Required Verific features
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
The following features, along with their corresponding Yosys build parameters,
|
|
are required for the Yosys-Verific patch:
|
|
|
|
* RTL elaboration with
|
|
* SystemVerilog with ``ENABLE_VERIFIC_SYSTEMVERILOG``, and/or
|
|
* VHDL support with ``ENABLE_VERIFIC_VHDL``.
|
|
* Hierarchy tree support and static elaboration with
|
|
``ENABLE_VERIFIC_HIER_TREE``.
|
|
|
|
Please be aware that the following Verific configuration build parameter needs
|
|
to be enabled in order to create the fully supported build:
|
|
|
|
::
|
|
|
|
database/DBCompileFlags.h:
|
|
DB_PRESERVE_INITIAL_VALUE
|
|
|
|
.. note::
|
|
|
|
Yosys+Verific builds may compile without these features, but we provide no
|
|
guarantees and cannot offer support if they are disabled or the Yosys-Verific
|
|
patch is not used.
|
|
|
|
Optional Verific features
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
The following Verific features are available with TabbyCAD and can be enabled in
|
|
Yosys builds:
|
|
|
|
* EDIF support with ``ENABLE_VERIFIC_EDIF``, and
|
|
* Liberty file support with ``ENABLE_VERIFIC_LIBERTY``.
|
|
|
|
Partially supported builds
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
This section describes Yosys+Verific configurations which we have confirmed as
|
|
working in the past, however they are not a part of our regular tests so we
|
|
cannot guarantee they are still functional.
|
|
|
|
To be able to compile Yosys with Verific, the Verific library must have support
|
|
for at least one HDL language with RTL elaboration enabled. The following table
|
|
lists a series of build configurations which are possible, but only provide a
|
|
limited subset of features. Please note that support is limited without YosysHQ
|
|
specific extensions of Verific library.
|
|
|
|
+--------------------------------------------------------------------------+---------------+------+-----------+--------------------+
|
|
| | Configuration values beginning with ENABLE_VERIFIC\_ |
|
|
+--------------------------------------------------------------------------+---------------+------+-----------+--------------------+
|
|
| Features | SYSTEMVERILOG | VHDL | HIER_TREE | YOSYSHQ_EXTENSIONS |
|
|
+==========================================================================+===============+======+===========+====================+
|
|
| SystemVerilog + RTL elaboration | 1 | 0 | 0 | 0 |
|
|
+--------------------------------------------------------------------------+---------------+------+-----------+--------------------+
|
|
| VHDL + RTL elaboration | 0 | 1 | 0 | 0 |
|
|
+--------------------------------------------------------------------------+---------------+------+-----------+--------------------+
|
|
| SystemVerilog + VHDL + RTL elaboration | 1 | 1 | 0 | 0 |
|
|
+--------------------------------------------------------------------------+---------------+------+-----------+--------------------+
|
|
| SystemVerilog + RTL elaboration + Static elaboration + Hier tree | 1 | 0 | 1 | 0 |
|
|
+--------------------------------------------------------------------------+---------------+------+-----------+--------------------+
|
|
| VHDL + RTL elaboration + Static elaboration + Hier tree | 0 | 1 | 1 | 0 |
|
|
+--------------------------------------------------------------------------+---------------+------+-----------+--------------------+
|
|
| SystemVerilog + VHDL + RTL elaboration + Static elaboration + Hier tree | 1 | 1 | 1 | 0 |
|
|
+--------------------------------------------------------------------------+---------------+------+-----------+--------------------+
|
|
|
|
.. note::
|
|
|
|
In case your Verific build has EDIF and/or Liberty support, you can enable
|
|
those options. These are not mentioned above for simplification and since
|
|
they are disabled by default.
|