Skip to content

Commit

Permalink
Docs: Clarify verific caveats
Browse files Browse the repository at this point in the history
  • Loading branch information
KrystalDelusion committed Aug 21, 2024
1 parent caffcce commit 11de4f3
Showing 1 changed file with 17 additions and 4 deletions.
21 changes: 17 additions & 4 deletions docs/source/yosys_internals/extending_yosys/build_verific.rst
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,21 @@ 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`_.
front-end tools. To license this patch for your own Yosys builds, `contact
YosysHQ`_.

.. warning::

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

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
Expand Down Expand Up @@ -62,6 +71,10 @@ To find the compile options used for a given Yosys build, call ``yosys-config
:start-at: --cxxflags
:end-before: --linkflags

.. note::

The YosysHQ specific extensions are only available with the TabbyCAD suite.

Required Verific features
~~~~~~~~~~~~~~~~~~~~~~~~~

Expand Down Expand Up @@ -110,7 +123,7 @@ 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 |
+--------------------------------------------------------------------------+-----+-----+-----+-----+
| Features | a | b | c | d |
Expand Down

0 comments on commit 11de4f3

Please sign in to comment.