[formal/doc] Add a getting started document for creating and running formal
This PR adds a getting started document to gether all instructions to
create and run FPV or connectivity tests in OpenTitan.
Signed-off-by: Cindy Chen <chencindy@opentitan.org>
diff --git a/doc/ug/getting_started/index.md b/doc/ug/getting_started/index.md
index 5d14a89..d1f56f5 100644
--- a/doc/ug/getting_started/index.md
+++ b/doc/ug/getting_started/index.md
@@ -44,6 +44,7 @@
| Verilator | Simulation Tool | SW Testing | no | no | [Getting Started with Verilator]({{< relref "getting_started_verilator.md" >}})|
| FPGA | FPGA Board | Testing & Evaluation | maybe (FPGA size dependent) | yes | [Getting Started on FPGAs]({{< relref "getting_started_fpga.md" >}}) |
| DV | Simulation Tool | HW Verification | yes | no | [Getting Started with Design Verification]({{< relref "getting_started_dv.md" >}}) |
+| Formal | Simulation Tool | HW Verification | yes | no | [Getting Started with Formal Verification]({{< relref "getting_started_formal.md" >}}) |
The instructions on how to compile the required demo software, and synthesize the main top-level hardware design ([Earl Grey]({{< relref "/hw/top_earlgrey" >}})) for each target are linked above in the table.
**Again, if you are new to the project, we recommend starting with the Verilator target, as this uses only free EDA tools, and does not require any additional hardware.**
diff --git a/doc/ug/getting_started_formal.md b/doc/ug/getting_started_formal.md
new file mode 100644
index 0000000..5fda38e
--- /dev/null
+++ b/doc/ug/getting_started_formal.md
@@ -0,0 +1,26 @@
+---
+title: "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]({{< 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:
+```console
+$ 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
+```
