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.

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. 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 want 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, set the YOSYS_VERIFIC_DIR CMake variable to point to the location where the library is located, e.g.

cmake -B build . -DYOSYS_VERIFIC_DIR="/usr/local/src/verific_lib"

During building, CMake will attempt to automatically detect available Verific library components to enable the corresponding compile-time option in Yosys. This can be overridden by manually setting the YOSYS_VERIFIC_FEATURES CMake variable. This variable should contain a semi-colon separated list, e.g. -DYOSYS_VERIFIC_FEATURES="systemverilog;hier_tree". The table below lists the features available to Yosys.

Feature	Directory	Description
systemverilog	verilog	SystemVerilog support
vhdl	vhdl	VHDL support
hier_tree	hier_tree	Hierarchy tree support
extensions	extensions	YosysHQ specific extensions support
edif	edif	EDIF support
liberty	synlib	Liberty file support

Note

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

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 systemverilog, and/or

  • VHDL support with vhdl.

• Hierarchy tree support and static elaboration with 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 will be automatically enabled in Yosys builds if the listed directory is included in the YOSYS_VERIFIC_DIR:

• EDIF support with edif directory, and

• Liberty file support with synlib directory.

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.

Features	YOSYS_VERIFIC_FEATURES
SystemVerilog + RTL elaboration	systemverilog
VHDL + RTL elaboration	vhdl
SystemVerilog + VHDL + RTL elaboration	systemverilog;vhdl
SystemVerilog + RTL elaboration + Static elaboration + Hier tree	systemverilog;vhdl;hier_tree
VHDL + RTL elaboration + Static elaboration + Hier tree	vhdl;hier_tree
SystemVerilog + VHDL + RTL elaboration + Static elaboration + Hier tree	systemverilog;vhdl;hier_tree

Note

In case your Verific build has EDIF and/or Liberty support, you can enable those options. These are not mentioned above for simplification.