Installation

There are two ways of installing the FVM:

Installing from pip

The recommended way of installing the FVM is to install it from the Python Package Index (PyPI), using pip:

pip3 install --pre fvm-formal

Here, we use the --pre flag to tell pip to include development and release candidate versions in its search. After 1.0.0 becomes stable, we can stop using the --pre flag.

Note

In recent pip versions you may need to create a python virtual environment (venv), or else you will get an “externally-managed-environment” error when trying to install packages using pip.

The following code:

python3 -m venv venv       # Create the venv in the venv folder
source venv/bin/activate   # Activate the newly created venv

will create a venv and activate it in the current shell. With the venv activated, pip3 install will install the FVM inside the venv.

See https://docs.python.org/3/tutorial/venv.html for details.

Installing from the git repository

Installing from the repository allows to perform an editable installation (passing the -e flag to pip3 install), so you can modify the python sources and the changes will be immediately available.

This option is also interesting if you want a specific version that was not tagged and pushed on PyPI, for example if you need to check out a specific commit, branch or tag.

git clone https://gitlab.com/fvmformal/fvm.git
pip3 install -e fvm

Note

The FVM is also available on github:

git clone https://github.com/fvmformal/fvm.git
pip3 install -e fvm

Note

The -e option tells python that the FVM sources reside in the recently cloned fvm directory. If you intend to remove that directory, you should remove the -e flag, but of course in that case the installation will not be editable.

Non-python dependencies

All python dependencies should be correctly managed by pip when you install the FVM. Nevertheless, there are two non-python dependencies which you should make sure you have in your system:

  • The actual formal tools: The FVM currently only supports the Questa formal tools (and the Questa OneSim simulator to compute simulation code coverage). You should have the tools installed in the system and the executables (qverify, vlib, vcom, vsim, etc) in your PATH, and of course a valid license.

  • Java: The FVM uses Allure Report to create beautiful HTML reports with the formal verification results. The FVM framework will download and use a specific release of Allure Report when needed. This framework is based on Java, so if you want to be able to create and view the reports you will need to install it, for example you can install the Open Java Development Kit (OpenJDK):

    • On Debian 13:

      sudo apt install openjdk-11-jre

    • On Rocky Linux 8:

      sudo yum install java-1.8.0-openjdk