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

    --cxxflags    -Wall -Wextra -ggdb -I"/usr/local/share/yosys/include" \
                      -MD -MP -D_YOSYS_ -fPIC -I/usr/local/include \
                      -DYOSYS_ENABLE_HELP_SOURCE -DYOSYS_VER=\"0.57\" \
                      -DYOSYS_MAJOR=0 -DYOSYS_MINOR=57 -DYOSYS_COMMIT=0.57 \
                      -std=c++17 -O3 -flto=thin -DYOSYS_ENABLE_READLINE \
                      -DYOSYS_ENABLE_PLUGINS -DYOSYS_ENABLE_GLOB \
                      -DYOSYS_ENABLE_ZLIB -I/usr/include/tcl8.6 \
                      -DYOSYS_ENABLE_TCL -DYOSYS_ENABLE_ABC \
                      -DVERIFIC_HIER_TREE_SUPPORT -DVERIFIC_SYSTEMVERILOG_SUPPORT \
                      -DVERIFIC_VHDL_SUPPORT -DVERIFIC_EDIF_SUPPORT \
                      -DVERIFIC_LIBERTY_SUPPORT -DYOSYSHQ_VERIFIC_EXTENSIONS \
                      -DYOSYS_ENABLE_VERIFIC -DYOSYS_ENABLE_COVER

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

1. ENABLE_VERIFIC_SYSTEMVERILOG

2. ENABLE_VERIFIC_VHDL

3. ENABLE_VERIFIC_HIER_TREE

4. ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS

	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

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.