Getting Started with Formal Verification

This document aims to enable a contributor to get started with a formal verification effort within the OpenTitan project. While most of the focus is on development of a testbench from scratch, it should also be useful to understand how to contribute to an existing effort.

Please refer to the OpenTitan Assertions for information on how formal verification is done in OpenTitan.

Formal property verification (FPV)

It is recommended to use the fpvgen tool to automatically create an FPV testbench template. To run the FPV tests in dvsim, please add the target in hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson, then run with command:

$ util/dvsim/dvsim.py hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson --select-cfgs {target_name}

It is recommended to add the FPV target to lint script hw/top_earlgrey/lint/top_earlgrey_fpv_lint_cfgs.hjson to quickly find typos.

Formal connectivity verification

The connectivity verification is mainly used for exhaustively verifying system-level connections. User can specify the connection ports via a CSV format file in hw/top_earlgrey/formal/conn_csvs folder. User can trigger top_earlgrey’s connectivity test using dvsim:

  util/dvsim/dvsim.py hw/top_earlgrey/formal/chip_conn_cfgs.hjson