| title: "Formal Verification Setup" |
| - /doc/ug/getting_started_formal |
| _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/README" >}}) for information on how formal verification is done in OpenTitan. |
| ## Formal property verification (FPV) |
| It is recommended to use the [fpvgen]({{< relref "util/fpvgen/README.md" >}}) 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/README" >}}) 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 |
