Formal verification flow

The tsfpga tools for formal verification allow you to run formal test cases without creating a SymbiYosys .sby file by hand. It also adds powerful features such as parallel runs, test filtering, XML reports, etc. The goal is to have an automated and scalable ecosystem where no configuration files are hand made, and all compile orders and dependencies are resolved automatically. It should also be module-centric so that the formal checks are defined locally in the modules, not in a central script.

tsfpga acts on top of several tools to run formal verification:

  • VUnit is used to handle compilation of the source files in correct order.

  • SymbiYosys runs the formal verification.

  • GHDL is used by VUnit to compile, and by SymbiYosys to synthesise the source code.

The role of tsfpga is to keep track of the project sources and checkers. It will generate a SymbiYosys .sby file for each formal project, with the correct settings and an updated source file list.

Formal checks are defined similarly to local simulation configurations, as described in Simulation flow. For formal checks, the setup_formal() method shall be overloaded in your module_*.py whenever you want to add a formal check. The checks are run using VUnit’s test runner, so the command line interface is similar to that of the simulation flow. It supports multiple formal checks in parallel, test filtering, verbosity level, XML reports, etc.

Minimal example

If the source code is roughly organized along the folder structure, running formal verification through tsfpga can be done with this script:

Minimal formal.py file.
from pathlib import Path
from tsfpga.module import get_modules
from tsfpga.formal_project import FormalProject

my_modules_folders = [
    Path("path/to/my/modules")
]

formal_project = FormalProject(
    modules=get_modules(my_modules_folders),
    project_path=Path("formal_project_path"))

for module in get_modules(my_modules_folders):
    module.setup_formal(formal_project)

formal_project.run()

A realistic example, used for tsfpga’s own checks, is available at examples/formal.py in the repo.

Formal checks need to be explicitly defined by implementing setup_formal() within each module:

Implementation of setup_formal().
from tsfpga.module import BaseModule


class Module(BaseModule):

    def setup_formal(self, formal_proj, **kwargs):
        formal_proj.add_config(
            top="example_top",
            generics=dict(some_generic=True),
            engine_command="smtbmc",
            solver_command="z3",
            depth=20,
            mode="prove")

Note

The top entity name must match its file name, so that example_top in this example is defined in a file named example_top.vhd.

Note

Settings for engine_command, solver_command, depth and mode options are described in the SymbiYosys documentation.

Generated .sby file

Below is an example generated .sby file, that is take from a formal check in the tsfpga repo.

Generated SymbiYosys .sby file.
[options]
mode prove
depth 20

[engines]
smtbmc z3

[script]
ghdl --std=08 -fpsl -P/repo/tsfpga/generated/formal_project/vunit_out/ghdl/libraries/math -P/repo/tsfpga/generated/formal_project/vunit_out/ghdl/libraries/axi -P/repo/tsfpga/generated/formal_project/vunit_out/ghdl/libraries/bfm -P/repo/tsfpga/generated/formal_project/vunit_out/ghdl/libraries/fifo -P/repo/tsfpga/generated/formal_project/vunit_out/ghdl/libraries/common -P/repo/tsfpga/generated/formal_project/vunit_out/ghdl/libraries/reg_file -P/repo/tsfpga/generated/formal_project/vunit_out/ghdl/libraries/resync axi_lite_reg_file_wrapper.vhd -e axi_lite_reg_file_wrapper
prep -top axi_lite_reg_file_wrapper

[files]
/repo/tsfpga/modules/math/src/unsigned_divider.vhd
/repo/tsfpga/modules/math/src/math_pkg.vhd
/repo/tsfpga/modules/axi/src/axi_read_cdc.vhd
/repo/tsfpga/modules/axi/src/axi_simple_crossbar.vhd
/repo/tsfpga/modules/axi/src/axi_write_cdc.vhd
/repo/tsfpga/modules/axi/src/axi_write_throttle.vhd
/repo/tsfpga/modules/axi/src/axi_b_fifo.vhd
/repo/tsfpga/modules/axi/src/axi_lite_pkg.vhd
/repo/tsfpga/modules/axi/src/axi_read_throttle.vhd
/repo/tsfpga/modules/axi/src/axi_address_fifo.vhd
/repo/tsfpga/modules/axi/src/axi_to_axi_lite.vhd
/repo/tsfpga/modules/axi/src/axi_r_fifo.vhd
/repo/tsfpga/modules/axi/src/axi_lite_to_vec.vhd
/repo/tsfpga/modules/axi/src/axi_lite_mux.vhd
/repo/tsfpga/modules/axi/src/axi_w_fifo.vhd
/repo/tsfpga/modules/axi/src/axi_lite_cdc.vhd
/repo/tsfpga/modules/axi/src/axi_lite_simple_crossbar.vhd
/repo/tsfpga/modules/axi/src/axi_pkg.vhd
/repo/tsfpga/modules/axi/src/axi_to_axi_lite_vec.vhd
/repo/tsfpga/modules/axi/src/axi_lite_pipeline.vhd
/repo/tsfpga/modules/fifo/src/asynchronous_fifo.vhd
/repo/tsfpga/modules/fifo/src/fifo.vhd
/repo/tsfpga/modules/fifo/rtl/fifo_netlist_build_wrapper.vhd
/repo/tsfpga/modules/common/src/addr_pkg.vhd
/repo/tsfpga/modules/common/src/common_pkg.vhd
/repo/tsfpga/modules/common/src/handshake_pipeline.vhd
/repo/tsfpga/modules/common/src/types_pkg.vhd
/repo/tsfpga/modules/common/src/attribute_pkg.vhd
/repo/tsfpga/modules/common/src/debounce.vhd
/repo/tsfpga/modules/common/src/handshake_splitter.vhd
/repo/tsfpga/modules/common/src/width_conversion.vhd
/repo/tsfpga/modules/reg_file/src/interrupt_register.vhd
/repo/tsfpga/modules/reg_file/src/axi_lite_reg_file.vhd
/repo/tsfpga/modules/reg_file/src/reg_file_pkg.vhd
/repo/tsfpga/modules/reg_file/rtl/axi_lite_reg_file_wrapper.vhd
/repo/tsfpga/modules/resync/src/resync_cycles.vhd
/repo/tsfpga/modules/resync/src/resync_slv_level_on_signal.vhd
/repo/tsfpga/modules/resync/src/resync_level_on_signal.vhd
/repo/tsfpga/modules/resync/src/resync_slv_level.vhd
/repo/tsfpga/modules/resync/src/resync_pulse.vhd
/repo/tsfpga/modules/resync/src/resync_level.vhd
/repo/tsfpga/modules/resync/src/resync_counter.vhd

It contains the settings (mode, depth, etc.) that were set in the module_*.py. The module list given to the FormalProject has been read to find a list of sources, that are then compiled with VUnit and GHDL. This forms the list of compiled libraries that is seen in the GHDL call under [script]. The file list [files] is also based on this list of modules.