yosys/docs/source/yosys_internals/extending_yosys/build_verific.rst

155 lines
6.9 KiB
ReStructuredText
Raw Normal View History

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
-----------------------
2024-08-21 17:03:59 -05:00
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
2024-08-21 17:04:00 -05:00
front-end tools. To license this patch for your own Yosys builds, `contact
YosysHQ`_.
2024-08-21 17:03:59 -05:00
.. warning::
2024-08-21 17:04:00 -05:00
While synthesis from RTL may be possible without this patch, YosysHQ provides
no guarantees of correctness and is unable to provide support.
We recommend against using unpatched Yosys+Verific builds in conjunction with
the formal verification front-end tools unless you are familiar with their inner
workings. There are cases where the tools will appear to work, while producing
incorrect results.
.. note::
2024-08-21 17:03:59 -05:00
Some of the formal verification front-end tools may not be fully supported
2024-08-21 17:03:59 -05:00
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
2024-08-21 17:03:59 -05:00
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
2024-08-21 17:04:00 -05:00
.. note::
The YosysHQ specific extensions are only available with the TabbyCAD suite.
2024-08-21 17:03:59 -05:00
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``.
2024-08-21 17:03:59 -05:00
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
2024-08-21 17:03:59 -05:00
.. note::
2024-08-21 17:03:59 -05:00
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.
2024-08-21 17:03:59 -05:00
Optional Verific features
~~~~~~~~~~~~~~~~~~~~~~~~~
2024-08-21 17:03:59 -05:00
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.
2024-08-21 17:03:59 -05:00
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.
2024-08-21 17:04:00 -05:00
+--------------------------------------------------------------------------+-----+-----+-----+-----+
| | Configuration values |
+--------------------------------------------------------------------------+-----+-----+-----+-----+
| Features | a | b | c | d |
+==========================================================================+=====+=====+=====+=====+
| 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 |
+--------------------------------------------------------------------------+-----+-----+-----+-----+
Configuration values:
a. ``ENABLE_VERIFIC_SYSTEMVERILOG``
b. ``ENABLE_VERIFIC_VHDL``
c. ``ENABLE_VERIFIC_HIER_TREE``
d. ``ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS``
.. 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.