What is FVM

Formal verification for VHDL, without the usual adoption barriers

FVM is the first publicly available, general-purpose, open-source formal verification methodology for VHDL designs. It combines a defined methodology, a helper tool to ease property writing, a build and test framework, and a repository of example designs. All fully documented!

A defined methodology

Ten steps, from linting to property checking and coverage collection, so you always know what to run next and why.

drom2psl

Turns WaveDrom timing diagrams into reusable PSL sequences, so properties are built from the test plan you already wrote.

A build and test framework

Six lines of Python run every tool, collect the results and generate reports for CI, the terminal and the browser.

Examples and training

Twelve designs of increasing complexity, plus documented techniques for reducing proof complexity when designs grow.

Who it is for

For engineers who write or verify VHDL

If you design or verify VHDL and want to use formal verification to increase the confidence in your designs, without duplicating your simulation effort, FVM is built for you. No prior formal experience is assumed: the examples start trivial and gradually grow in complexity.

Methodology

From linting to signoff coverage

The automated tools run first, so you start finding issues while you are still writing properties. Property checking and coverage collection follow. The framework runs every step, in order, and reports the results.

Automatic tools

No properties needed. You can optionally specify clock and reset domains.

lint Static checks for potential issues Questa Lint
friendliness Estimate suitability for formal verification Questa AutoCheck
rulecheck Find deadlocks, overflows and similar issues Questa AutoCheck
xverify Study how unknown values propagate Questa X-Check
reachability Detect uncoverable elements Questa CoverCheck
resets Find reset domain crossing issues Questa RDC
clocks Find clock domain crossing issues Questa CDC

Your properties

Written as assert, assume and cover directives.

prove Prove or disprove your properties Questa PropCheck
prove.formalcover Compute formal code coverage Questa PropCheck
prove.simcover Simulation coverage from reached covers Questa Simulator

Six lines of Python run it all

The framework sits between you and the tools. Add your sources, set the toplevel, call run(). It generates the tool scripts, runs them, and produces reports: for the terminal, for CI systems, and for the browser.

from fvm import FvmFramework

fvm = FvmFramework()
fvm.add_vhdl_sources("examples/uart_tx/*.vhd")
fvm.add_psl_sources("examples/uart_tx/*.psl")
fvm.set_toplevel("uart_tx")
fvm.run()

Results

Comes with twelve example designs, from a counter to an IPv6 transceiver

A number of examples of increasing complexity, each one verified with the methodology. Formal verification found real bugs in designs that had already passed simulation.

40/40 assertions proven on the IPv6 transceiver, the most complex design in the repository
~200h to verify eight of the examples, part-time, by a junior engineer
3 new bugs found in designs that had already been verified by simulation

Asynchronous FIFO

With a specific frequency relation between read and write clocks, a reset on the write side could underflow the FIFO.

IPv6 transceiver

Some IPv6 headers carried incorrect values, caused by a problem in the top-level glue logic.

AXI4-Lite slave

Returns correct data but signals an error in the last cycle of a timeout period, likely an off-by-one in the timeout counter or condition.

For real industry designs

Successfully applied to very complex designs

Apart from the repository of examples, FVM has been successfully applied to real industrial cases.

+300k state bits in ESA's SpaceFibre Port IP Core
13 different memories in ESA's SpaceFibre IP core
>1M state bits in Gaisler's L2 Cache

SpaceFibre Port IP Core

SpaceFibre Port with Interface Layer, Lane Layer, Data Link Layer, Broadcast Layer, and Virtual Channel Layer.

Gaisler's FOSS L2 Cache

Level-2 cache controller from the GRLIB IP Library.

Getting started

Install it and run your first example

The framework is a Python package. Install it into a virtual environment, then follow the documentation to set up your first design.

Installation guide Your first example

pip3 install fvm-formal

You will also need the Questa formal tools with a valid license, and Java for the HTML reports

Publications

Open access

FVM: A Formal Verification Methodology for VHDL Designs

Hipólito Guzmán-Miranda, Marcos López García and Alberto Urbón Aguado · IEEE Open Journal of the Computer Society, vol. 6, pp. 1920–1933, 2025

Read the paper

@article{FVM_methodology,
  author    = {Hipólito {Guzmán-Miranda} and Marcos {López García} and Alberto {Urbón Aguado}},
  title     = {{FVM}: {A} {F}ormal {V}erification {M}ethodology for {VHDL} designs},
  journal   = {IEEE Open Journal of the Computer Society},
  url       = {https://ieeexplore.ieee.org/document/11217165},
  year      = {2025},
  volume    = {6},
  number    = {},
  pages     = {1920-1933},
  keywords  = {Formal verification;Field programmable gate arrays;VHDL;Complexity theory;Market research;European Space Agency;Europe;Computer bugs;Codes;Clocks;Formal verification;verification methodology;VHDL;PSL;ASIC;FPGA},
  doi       = {10.1109/OJCS.2025.3625468}
  }

See the full list of publications in the documentation

Repository

Open source, under Apache 2.0

Development happens on GitLab. The GitHub repository is a mirror, so issues and merge requests belong on GitLab.

GitLab repository GitHub mirror

git clone https://gitlab.com/fvmformal/fvm.git

Also published on PyPI as fvm-formal.

Team

Developed at Universidad de Sevilla

FVM is developed and maintained by:

Hipólito Guzmán Miranda

Universidad de Sevilla
hguzman@us.es

Marcos López García

Universidad de Sevilla
marlopgar40@alum.us.es

With the support and guidance of

Alberto Urbón Aguado

European Space Agency
Technical Officer