Before following this guide, make sure you've followed the [dependency installation and software build instructions]({{< relref “getting_started” >}}).
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]({{< relref “hw/formal/doc” >}}) for information on how formal verification is done in OpenTitan.
It is recommended to use the [fpvgen]({{< relref “util/fpvgen/doc” >}}) 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]({{< relref “hw/lint/doc” >}}) script hw/top_earlgrey/lint/top_earlgrey_fpv_lint_cfgs.hjson to quickly find typos.
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