[fpv] V2S formal support

This PR sets up the FPV environment to support V2S formal:
1). Add a `task` enviornment input to indicate which subsets of
  assertions to run.
2). Relax original `prim_assert_sec_cm.svh` alert timing because FPV
  might trigger other fatal alerts.
3). Enable the FPV checks in sram_ctrl.

Signed-off-by: Cindy Chen <chencindy@opentitan.org>

hw/formal/tools/dvsim/common_fpv_cfg.hjson

diff --git a/hw/formal/tools/dvsim/common_fpv_cfg.hjson b/hw/formal/tools/dvsim/common_fpv_cfg.hjson
index 8f28dd2..2e11665 100644
--- a/hw/formal/tools/dvsim/common_fpv_cfg.hjson
+++ b/hw/formal/tools/dvsim/common_fpv_cfg.hjson
@@ -5,9 +5,11 @@
   sub_flow:    fpv
   import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_formal_cfg.hjson"]
   stopats: ""
+  task: ""
 
   // Optional vars that need to exported to the env
   exports: [
-    {STOPATS: '{stopats}'}
+    {STOPATS: '{stopats}'},
+    {TASK:    '{task}'}
   ]
 }

hw/formal/tools/jaspergold/fpv.tcl

diff --git a/hw/formal/tools/jaspergold/fpv.tcl b/hw/formal/tools/jaspergold/fpv.tcl
index 7df9328..bd2805e 100644
--- a/hw/formal/tools/jaspergold/fpv.tcl
+++ b/hw/formal/tools/jaspergold/fpv.tcl
@@ -2,6 +2,15 @@
 # Licensed under the Apache License, Version 2.0, see LICENSE for details.
 # SPDX-License-Identifier: Apache-2.0
 
+# Environment varibles:
+# CHECK: flag to turn on or off conflict and deadloop checks.
+# COMMON_MSG_TCL_PATH: string to indicate the path to `jaspergold_common_message_process.tcl` file,
+#                      which sets common message configurations.
+# COV: flag to turn on or off coverage collection.
+# DUT_TOP: string to indicate the top-level module name.
+# STOPATS: string to indicate the name of the signal to insert `stopat`.
+# TASK: string to collect and prove a subset of assertions that contains these string.
+
 # clear previous settings
 clear -all
 
@@ -16,10 +25,18 @@
 # read design
 #-------------------------------------------------------------------------
 
-# only one scr file exists in this folder
-analyze -sv09     \
-  +define+FPV_ON  \
-  -f [glob *.scr]
+if {$env(TASK) == "FpvSecCm"} {
+  analyze -sv09 \
+    +define+FPV_ON \
+    +define+FPV_SEC_CM_ON \
+    -bbox_m prim_count \
+    -bbox_m prim_double_lfsr \
+    -f [glob *.scr]
+} else {
+  analyze -sv09 \
+    +define+FPV_ON \
+    -f [glob *.scr]
+}
 
 if {$env(DUT_TOP) == "prim_count_tb"} {
   elaborate -top $env(DUT_TOP) \
@@ -148,13 +165,6 @@
 # Input scanmode_i should not be X
 assume -from_assert -remove_original -regexp {^\w*\.scanmodeKnown}
 
-# TODO: If scanmode is set to 0, then JasperGold errors out complaining
-# about combo loops, which should be debugged further. For now, below
-# lines work around this issue
-if {$env(DUT_TOP) == "top_earlgrey"} {
-  assume {scanmode_i == 1}
-}
-
 # run once to check if assumptions have any conflict
 if {[info exists ::env(CHECK)]} {
   if {$env(CHECK)} {
@@ -164,6 +174,12 @@
   }
 }
 
+# If `TASK` variable is set, choose the subset of assertions that contain ${TASK} in their
+# assertion names.
+if {$env(TASK) ne ""} {
+  task -create $env(TASK) -source_task <embedded> -copy *$env(TASK)* -copy_assumes -set
+}
+
 # TODO: support the following feature.
 # Uncomment "jg_auto_coi_cov_waivers" to automatically waive out COI cover items which cannot
 # propagate to "relevant signals" (by default, top instance outputs). If you need to specify
@@ -181,9 +197,15 @@
 # prove all assertions & report
 #-------------------------------------------------------------------------
 
-# time limit set to 2 hours
 get_reset_info -x_value -with_reset_pin
-prove -all -time_limit 2h
+
+# time limit set to 2 hours
+if {$env(TASK) ne ""} {
+  prove -task $env(TASK) -time_limit 2h
+} else {
+  prove -all -time_limit 2h
+}
+
 report
 
 #-------------------------------------------------------------------------

hw/ip/prim/rtl/prim_alert_sender.sv

diff --git a/hw/ip/prim/rtl/prim_alert_sender.sv b/hw/ip/prim/rtl/prim_alert_sender.sv
index 4bb4c6a..e306384 100644
--- a/hw/ip/prim/rtl/prim_alert_sender.sv
+++ b/hw/ip/prim/rtl/prim_alert_sender.sv
@@ -374,4 +374,11 @@
       clk_i, !rst_ni || (alert_tx_o.alert_p == alert_tx_o.alert_n))
 `endif
 
+`ifdef FPV_SEC_CM_ON
+  // Assumptions for FPV security countermeasures to ensure the alert protocol functions collectly.
+  `ASSUME_FPV(AckPFollowsAlertP_S, alert_rx_i.ack_p == $past(alert_tx_o.alert_p))
+  `ASSUME_FPV(AckNFollowsAlertN_S, alert_rx_i.ack_n == $past(alert_tx_o.alert_n))
+  `ASSUME_FPV(TriggerAlertInit_S, $stable(rst_ni) == 0 |=> alert_rx_i.ping_p == alert_rx_i.ping_n)
+  `ASSUME_FPV(PingDiffPair_S, ##2 alert_rx_i.ping_p != alert_rx_i.ping_n)
+`endif
 endmodule : prim_alert_sender

hw/ip/prim/rtl/prim_assert_sec_cm.svh

diff --git a/hw/ip/prim/rtl/prim_assert_sec_cm.svh b/hw/ip/prim/rtl/prim_assert_sec_cm.svh
index 4f5da10..92a44be 100644
--- a/hw/ip/prim/rtl/prim_assert_sec_cm.svh
+++ b/hw/ip/prim/rtl/prim_assert_sec_cm.svh
@@ -9,19 +9,20 @@
 
 // Helper macros
 `define ASSERT_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_, ERR_NAME_) \
-  `ASSERT(NAME_, $rose(PRIM_HIER_.ERR_NAME_) |-> ##[1:MAX_CYCLES_] $rose(ALERT_.alert_p)) \
+  `ASSERT(FpvSecCm``NAME_``, $rose(PRIM_HIER_.ERR_NAME_) |-> ##[0:MAX_CYCLES_] (ALERT_.alert_p)) \
   `ifdef INC_ASSERT \
   assign PRIM_HIER_.unused_assert_connected = 1'b1; \
-  `endif
+  `endif \
+  `ASSUME_FPV(ErrTriggerAfterAlertInit_S, $stable(rst_ni) == 0 |-> PRIM_HIER_.ERR_NAME_ == 0 [*10])
 
 // macros for security countermeasures
-`define ASSERT_PRIM_COUNT_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_ = 5) \
+`define ASSERT_PRIM_COUNT_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_ = 7) \
   `ASSERT_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_, err_o)
 
-`define ASSERT_PRIM_DOUBLE_LFSR_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_ = 5) \
+`define ASSERT_PRIM_DOUBLE_LFSR_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_ = 7) \
   `ASSERT_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_, err_o)
 
-`define ASSERT_PRIM_FSM_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_ = 5) \
+`define ASSERT_PRIM_FSM_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_ = 7) \
   `ASSERT_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_, unused_valid_st)
 
 `endif // PRIM_ASSERT_SEC_CM_SVH

hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson

diff --git a/hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson b/hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson
index b9a0eaa..da5032b 100644
--- a/hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson
+++ b/hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson
@@ -592,6 +592,7 @@
                import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"]
                rel_path: "hw/ip/sram_ctrl/{sub_flow}/{tool}"
                cov: false
+               task: "FpvSecCm"
              }
              { name: sysrst_ctrl
                dut: sysrst_ctrl