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

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 1       YosysHQ specific extensions support
ENABLE_VERIFIC_EDIF               0       EDIF support
ENABLE_VERIFIC_LIBERTY            0       Liberty file support
================================= ======= ===================================

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
~~~~~~~~~~~~~~~~~~~~~~~~~~

.. todo:: still unclear on the purpose of this section.

   Are these the configurations we have tested as being able to compile?

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.