[doc/fpv] Add doc on how to create a FPV security check env
This PR adds a section under formal README to document how to create a
FPV environment to test common security countermeasures.
Signed-off-by: Cindy Chen <chencindy@opentitan.org>
diff --git a/hw/dv/sv/cip_lib/doc/index.md b/hw/dv/sv/cip_lib/doc/index.md
index 2044f83..dd44bd1 100644
--- a/hw/dv/sv/cip_lib/doc/index.md
+++ b/hw/dv/sv/cip_lib/doc/index.md
@@ -496,8 +496,9 @@
Note: The `sim_tops` in sim_cfg.hjson should be updated to include this bind file.
### Security Verification for common countermeasure primitives
-A [security countermeasure verification framework]({{< relref "doc/ug/sec_cm_dv_framework" >}}) is implemented in cip_lib to verify common countermeasure primitives in a semi-uutomated way.
+A [security countermeasure verification framework]({{< relref "doc/ug/sec_cm_dv_framework" >}}) is implemented in cip_lib to verify common countermeasure primitives in a semi-automated way.
+#### Design Verification
cip_lib imports [sec_cm_pkg](https://github.com/lowRISC/opentitan/tree/master/hw/dv/sv/sec_cm), which automatically locates all the common countermeasure primitives and binds an interface to each of them.
In the cib_base_vseq, it injects a fault to each of these primitives and verifies that the fault will lead to a fatal alert.
The details of the sequences can be found in testplans - [sec_cm_count_testplan](https://github.com/lowRISC/opentitan/blob/master/hw/dv/tools/dvsim/testplans/sec_cm_count_testplan.hjson), [sec_cm_fsm_testplan](https://github.com/lowRISC/opentitan/blob/master/hw/dv/tools/dvsim/testplans/sec_cm_fsm_testplan.hjson) and [sec_cm_double_lfsr_testplan](https://github.com/lowRISC/opentitan/blob/master/hw/dv/tools/dvsim/testplans/sec_cm_double_lfsr_testplan.hjson).
@@ -599,3 +600,6 @@
endcase
endfunction: sec_cm_fi_ctrl_svas
```
+
+#### Formal Verification
+Please refer to [formal document]({{< relref "hw/formal/README" >}}) on how to create a FPV environment for common countermeasures.
diff --git a/hw/formal/README.md b/hw/formal/README.md
index 3339c70..45df26e 100644
--- a/hw/formal/README.md
+++ b/hw/formal/README.md
@@ -269,6 +269,49 @@
```
Adding a `--gui` option will open the JaperGold GUI.
+## Running FPV on security blocks for common countermeasure primitives
+A [security countermeasure verification framework]({{< relref "doc/ug/sec_cm_dv_framework" >}}) is implemented in design and fpv tcl script to verify common countermeasure primitives in a semi-automated way.
+
+### Common security assertion macros
+OpenTitan's security IP blocks have implemented assertions to check against common fault injections.
+These assertions ensure if the security prim module returns an error, a corresponding alert should fire immediately without any gating conditions.
+There are three pre-defined assertion macros under file `hw/ip/prim/rtl/prim_assert_sec_cm.svh`:
+* ASSERT_PRIM_FSM_TRIGGER_ALERT: if design module `prim_sparse_fsm_flop` returns `state_o` value that is not one of the defined FSM states, which means the FSM state might be attacked, a fatal alert is expected to fire.
+* ASSERT_PRIM_COUNT_TRIGGER_ALERT: if design module `prim_count` sets `err_o` to 1, which means the two counters do not match, a fatal alert is expected to fire.
+* ASSERT_PRIM_DOUBLE_LFSR_TRIGGER_ALERT: if design module `prim_double_lfsr` sets `err_o` to 1, which means two LFSR states do not match, a fatal alert is expected to fire.
+Note that assertions defined with these macros will have a common prefix name `FpvSecCm`, which will help the FPV tcl file to group them in a specific task.
+
+### FPV fault injection
+The above security assertions are expected to be unreachable in normal design environment, and are only reachable if a fault is injected.
+To create a FPV environment that has fault injections, the `stopat` command and black box methods are used.
+* FSM fault injection: a `stopat` is placed at `state_o` output.
+* Counter fault injection: black-box the prim_count module.
+* Double LFSR fault injection: black-box the prim_double_lfsr module.
+Then we will let formal environment to randomly drive these outputs and run security assertions to ensure these error cases will trigger alerts under any circumstance.
+
+### Set up FPV security check environment
+To set up the FPV security check environment, please follow the steps below:
+1. Add an item under `hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson` with the naming convention "{ip_name}_sec_cm".
+2. Under the item add an entry "task" with value "FpvSecCm".
+This entry tells the tcl file to black-box security prim modules in the FPV environment, and define required macros.
+This "task" entry also tells the tcl file to disable regular assertions and only analyze macro defined security assertions with prefix `FpvSecCm`.
+3. Under the item add an entry "stopats" if design has sparse FSMs.
+This is an optional step. If design contains more than one stopat path, user can input them with bracket `stopat: "{path1}, {path2}"`.
+
+Here is an example on csrng module:
+```
+{
+ name: csrng_sec_cm
+ dut: csrng
+ fusesoc_core: lowrisc:dv:csrng_sva
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
+ rel_path: "hw/ip/csrng/{sub_flow}/{tool}"
+ cov: false
+ task: "FpvSecCm"
+ stopats: "*u_state_regs.state_o"
+}
+```
+
## Naming Conventions
For assertions, it is preferred to use postfix `_A` for assertions, `_M` for assumptions, `_P` for properties, and `_S` for sequences.
For example:
