[alert,fpv] Dramatic improvements to the async alert fpv

hw/formal/tools/jaspergold/fpv.tcl

@@ -77,6 +77,17 @@ if {[info exists ::env(PARAMS)]} {
     }
 }
 
+# Chains of successive A ##1 B ##1 C ... in sequences can take a long time to elaborate. There is a
+# new flag to elaborate called -optimize_implication_assert which improves this, but it only appears
+# from Jasper 2023.06. Call the get_version function to figure out whether we've got the right
+# version: it should be 2023.06, 2023.09, 2023.12 or something that starts with a later year
+# (202[4-9] or 20[3-9].)
+if {[regexp "^\(20\[3-9\]\[0-9\]\)\|\(202\[4-9\]\)\|\(2023\.\(0\[69\]\)\|12\)" [get_version]]} {
+  set oia_arg "-optimize_implication_assert"
+} else {
+  set oia_arg ""
+}
+
 if {$env(DUT_TOP) == "prim_count_tb"} {
     append elab_args " -param ResetValue $ResetValue"
 }
@@ -85,7 +96,7 @@ if {$env(DUT_TOP) == "prim_count_tb"} {
 # to the elaborate command.
 eval elaborate -top $env(DUT_TOP) \
                -enable_sva_isunknown -disable_auto_bbox \
-               ${elab_args}
+               ${oia_arg} ${elab_args}
 
 set stopat [regexp -all -inline {[^\s\']+} $env(STOPATS)]
 if {$stopat ne ""} {
@@ -97,6 +108,11 @@ if {$stopat ne ""} {
 # no initial phases if the scripts do not).
 set pre_phases 0
 
+# Also set the cov_tasks variable to just <embedded> (which says to include properties that were
+# read from SystemVerilog when calculating coverage). AFTER_LOAD scripts may add extra tasks
+# (because they needed e.g. a stopat).
+set cov_tasks "<embedded>"
+
 if {[info exists ::env(AFTER_LOAD)]} {
     set flist $env(AFTER_LOAD)
     foreach file $flist {
@@ -272,12 +288,14 @@ report
 #-------------------------------------------------------------------------
 
 if {$env(COV) == 1} {
-  check_cov -measure -all -time_limit 2h
-  # Waive the synthesis_optimized cover items
-  set file $env(JG_TCL_DIR)/synthesis_optimized.tcl
-  puts "Waiving items optimized in synthesis from $file"
-  source $file
-  check_cov -report -force -exclude { reset waived }
-  check_cov -report -no_return -report_file cover.html \
-      -html -force -exclude { reset waived }
+    check_cov -measure -tasks ${cov_tasks} -time_limit 2h
+
+    # Waive the synthesis_optimized cover items
+    set file $env(JG_TCL_DIR)/synthesis_optimized.tcl
+    puts "Waiving items optimized in synthesis from $file"
+    source $file
+
+    check_cov -report -task ${cov_tasks} -force -exclude { reset waived }
+    check_cov -report -no_return -report_file cover.html -task ${cov_tasks} \
+                      -html -force -exclude { reset waived }
 }

hw/ip/prim/fpv/prim_alert_rxtx_async_fatal_fpv.core

@@ -9,6 +9,7 @@ filesets:
     depend:
       - lowrisc:prim:all
       - lowrisc:prim:alert
+      - lowrisc:fpv:prim_diff_decode_fpv
     files:
       - vip/prim_alert_rxtx_async_assert_fpv.sv
       - tb/prim_alert_rxtx_async_fatal_tb.sv

hw/ip/prim/fpv/prim_alert_rxtx_async_fpv.core

@@ -9,6 +9,7 @@ filesets:
     depend:
       - lowrisc:prim:all
       - lowrisc:prim:alert
+      - lowrisc:fpv:prim_diff_decode_fpv
     files:
       - vip/prim_alert_rxtx_async_assert_fpv.sv
       - tb/prim_alert_rxtx_async_tb.sv

hw/ip/prim/fpv/prim_alert_rxtx_fatal_fpv.core

@@ -9,6 +9,7 @@ filesets:
     depend:
       - lowrisc:prim:all
       - lowrisc:prim:alert
+      - lowrisc:fpv:prim_diff_decode_fpv
     files:
       - vip/prim_alert_rxtx_assert_fpv.sv
       - tb/prim_alert_rxtx_fatal_tb.sv

hw/ip/prim/fpv/prim_alert_rxtx_fpv.core

@@ -9,6 +9,7 @@ filesets:
     depend:
       - lowrisc:prim:all
       - lowrisc:prim:alert
+      - lowrisc:fpv:prim_diff_decode_fpv
     files:
       - vip/prim_alert_rxtx_assert_fpv.sv
       - tb/prim_alert_rxtx_tb.sv

hw/ip/prim/fpv/prim_diff_decode_fpv.core

@@ -0,0 +1,29 @@
+CAPI=2:
+# Copyright lowRISC contributors (OpenTitan project).
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+name: "lowrisc:fpv:prim_diff_decode_fpv"
+description: "A binding with assertions for prim_diff_decode_fpv"
+filesets:
+  files_formal:
+    depend:
+      - lowrisc:prim:diff_decode
+    files:
+      - tb/prim_diff_decode_bind_fpv.sv
+      - vip/prim_diff_decode_assert_fpv.sv
+    file_type: systemVerilogSource
+
+targets:
+  default: &default_target
+    # note, this setting is just used
+    # to generate a file list for jg
+    default_tool: icarus
+    filesets:
+      - files_formal
+
+  formal:
+    <<: *default_target
+
+  lint:
+    <<: *default_target

hw/ip/prim/fpv/tb/prim_diff_decode_bind_fpv.sv

@@ -0,0 +1,10 @@
+// Copyright lowRISC contributors (OpenTitan project).
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+// Bind prim_diff_decode_assert_fpv into each instance of prim_diff_decode in the design.
+
+module prim_diff_decode_bind_fpv;
+  bind prim_diff_decode prim_diff_decode_assert_fpv
+    #(.AsyncOn (AsyncOn)) u_assert_fpv (.clk_i, .rst_ni);
+endmodule

hw/ip/prim/fpv/tb/rxtx_after_load.tcl

@@ -0,0 +1,36 @@
+# Copyright lowRISC contributors (OpenTitan project).
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+# This is a TCL file that can be sourced by FPV runs that are doing
+# some form of "prim_alert_rxtx" verification.
+
+proc move_to_task {task_name assert_name} {
+    task -edit ${task_name} -copy "${assert_name}*"
+    assert -disable ${assert_name}
+}
+
+
+set valid_state_props [get_property_list -regexp -include {"name" "ValidState_A$"}]
+foreach prop $valid_state_props {
+    assert -set_helper $prop
+}
+
+# The property names in this list are properties that depend on some FSM state register pointing at
+# a parasitic state. Use a stopat on various state registers to make the properties say something.
+
+task -create FreeFsm
+stopat -task FreeFsm "i_prim_alert_sender.state_q"
+stopat -task FreeFsm "i_prim_alert_receiver.state_q"
+
+set parasitic_state_props {SenderStateDValid_A ReceiverStateDValid_A}
+
+foreach psn $parasitic_state_props {
+    foreach psp [get_property_list -regexp -include [list name "${psn}$"]] {
+        move_to_task FreeFsm $psp
+    }
+}
+
+# Add FreeFsm to the cov_tasks variable, which is a list of the tasks that will be used for
+# check_cov at the end of fpv.tcl if coverage is enabled.
+lappend cov_tasks FreeFsm

hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert_fpv.sv

@@ -34,6 +34,9 @@ module prim_alert_rxtx_async_assert_fpv
   input        alert_o
 );
 
+  default clocking @(posedge clk_i); endclocking
+  default disable iff !rst_ni;
+
   import prim_mubi_pkg::mubi4_test_true_strict;
 
   logic error_present;
@@ -47,9 +50,10 @@ module prim_alert_rxtx_async_assert_fpv
                         prim_alert_rxtx_async_tb.i_prim_alert_receiver.InitReq,
                         prim_alert_rxtx_async_tb.i_prim_alert_receiver.InitAckWait};
 
-  logic sender_is_idle, receiver_is_idle, sender_is_pinging;
+  logic sender_is_idle, receiver_is_idle, both_idle, sender_is_pinging;
   assign sender_is_idle = i_prim_alert_sender.state_q == i_prim_alert_sender.Idle;
   assign receiver_is_idle = i_prim_alert_receiver.state_q == i_prim_alert_receiver.Idle;
+  assign both_idle = sender_is_idle && receiver_is_idle;
   assign sender_is_pinging = i_prim_alert_sender.state_q inside
                              {i_prim_alert_sender.PingHsPhase1, i_prim_alert_sender.PingHsPhase2};
 
@@ -66,11 +70,16 @@ module prim_alert_rxtx_async_assert_fpv
   logic error_setreg_d, error_setreg_q;
   assign error_setreg_d = error_present | error_setreg_q;
 
+  logic seen_skew_d, seen_skew_q;
+  assign seen_skew_d = seen_skew_q | |{ping_skew_i, ack_skew_i, alert_skew_i};
+
   always_ff @(posedge clk_i or negedge rst_ni) begin : p_reg
     if (!rst_ni) begin
       error_setreg_q <= 1'b0;
+      seen_skew_q    <= 1'b0;
     end else begin
       error_setreg_q <= error_setreg_d;
+      seen_skew_q    <= seen_skew_d;
     end
   end
 
@@ -85,34 +94,61 @@ module prim_alert_rxtx_async_assert_fpv
   `ASSUME_FPV(PingEn_M, $rose(ping_req_i) |-> ping_req_i throughout
       (ping_ok_o || error_present)[->1] ##1 $fell(ping_req_i))
 
-  // Note: the sequence lengths of the handshake and the following properties needs to
-  // be parameterized accordingly if different clock ratios are to be used here.
-  // TODO: tighten bounds if possible
-  sequence FullHandshake_S;
-    $rose(prim_alert_rxtx_async_tb.alert_pd)   ##[3:6]
-    $rose(prim_alert_rxtx_async_tb.ack_pd)     &&
-    $stable(prim_alert_rxtx_async_tb.alert_pd) ##[3:6]
-    $fell(prim_alert_rxtx_async_tb.alert_pd)   &&
-    $stable(prim_alert_rxtx_async_tb.ack_pd)   ##[3:6]
-    $fell(prim_alert_rxtx_async_tb.ack_pd)     &&
-    $stable(prim_alert_rxtx_async_tb.alert_pd);
-  endsequence
-
-  // note: injected errors may lockup the FSMs, and hence the full HS can
-  // only take place if both FSMs are in a good state
-  `ASSERT(PingHs_A, ##1 $changed(prim_alert_rxtx_async_tb.ping_pd) &&
-      sender_is_idle && receiver_is_idle |-> ##[0:5] FullHandshake_S,
-      clk_i, !rst_ni || error_setreg_q || init_pending)
-  `ASSERT(AlertHs_A, alert_req_i &&
-      sender_is_idle && receiver_is_idle |-> ##[0:5] FullHandshake_S,
-      clk_i, !rst_ni || error_setreg_q || init_pending)
-  `ASSERT(AlertTestHs_A, alert_test_i &&
-      sender_is_idle && receiver_is_idle |-> ##[0:5] FullHandshake_S,
-      clk_i, !rst_ni || error_setreg_q || init_pending)
-  // Make sure we eventually get an ACK
-  `ASSERT(AlertReqAck_A, alert_req_i &&
-      sender_is_idle && receiver_is_idle |-> strong(##[1:$] alert_ack_o),
-      clk_i, !rst_ni || error_setreg_q || init_pending)
+  // The alert signal being sent from the alert sender
+  logic sender_alert_level;
+  assign sender_alert_level = i_prim_alert_sender.alert_tx_o.alert_p &
+                              ~i_prim_alert_sender.alert_tx_o.alert_n;
+
+  // The alert sender's view of the ack signal that was sent from the alert receiver.
+  logic sender_ack_level;
+  assign sender_ack_level = i_prim_alert_sender.alert_rx_i.ack_p &
+                            ~i_prim_alert_sender.alert_rx_i.ack_n;
+
+  // The ping signal being sent from the alert receiver
+  logic receiver_ping_level;
+  assign receiver_ping_level = i_prim_alert_receiver.alert_rx_o.ping_p &
+                               ~i_prim_alert_receiver.alert_rx_o.ping_n;
+
+  // Handshake assertions
+  //
+  // These assertions track "handshakes". Normally this has the sender signalling something and the
+  // receiver responding, but the ping handshake goes the other way around. To avoid situations
+  // where the blocks are starting in the wrong state, the precondition for the assertions requires
+  // both sender and receiver to be in the idle state.
+  //
+  // The "if (1)" part is to provide a block that can hold the "default disable iff" setting.
+  if (1) begin : g_handshake_assertions
+    // Assertions about handshakes should be disabled if any error has been injected into the
+    // signals (either by forcing a bit or by including a nonzero skew). Injecting errors onto the
+    // bus can stop the handshake working, but that isn't the behaviour we're trying to reason
+    // about.
+    default disable iff !rst_ni || error_setreg_d || seen_skew_d || init_pending;
+
+    // The full alert handshake is as follows:
+    //
+    //  - The sender raises the alert signal and then holds it high
+    //  - The receiver sees the alert and raises the ack signal, holding that high.
+    //  - The sender sees the ack and drops the alert signal again
+    //  - The receiver sees that the alert has dropped and drops its ack.
+    //
+    // We monitor it from the point of view of the alert sender, so look at the alert signal that it
+    // transmits and the ack signal that it receives.
+    sequence FullHandshake_S;
+      $rose(sender_alert_level) ##1 $stable(sender_alert_level)[*1:5] ##0
+      $rose(sender_ack_level)   ##1 $stable(sender_ack_level)[*1:5]   ##0
+      $fell(sender_alert_level) ##1 $stable(sender_alert_level)[*1:5] ##0
+      $fell(sender_ack_level);
+    endsequence
+
+    PingHs_A: assert property (##1 $changed(receiver_ping_level) && both_idle |=>
+                               ##[0:4] FullHandshake_S);
+
+    AlertHs_A: assert property (alert_req_i && both_idle |-> ##[0:5] FullHandshake_S);
+
+    AlertTestHs_A: assert property (alert_test_i && both_idle |-> ##[0:5] FullHandshake_S);
+
+    AlertReqAck_A: assert property (alert_req_i && both_idle |=> s_eventually alert_ack_o);
+  end
 
   // Transmission of pings
   //
@@ -151,22 +187,32 @@ module prim_alert_rxtx_async_assert_fpv
       !ping_req_i [*10] ##1 ($rose(alert_req_i) || $rose(alert_test_i)) && sender_is_idle |->
       ##[3:5] alert_o,
       clk_i, !rst_ni || ping_req_i || error_setreg_q || init_pending || alert_skew_i || ack_skew_i)
-  // eventual transmission of alerts in the general case which can include continous ping
-  // collisions
-  `ASSERT(AlertCheck1_A,
-      alert_req_i || alert_test_i |-> strong(##[1:$] sender_is_idle ##[3:5] alert_o),
-      clk_i, !rst_ni || error_setreg_q ||
-      prim_alert_rxtx_async_tb.i_prim_alert_sender.alert_clr || init_pending)
+
+  // If the sender is asked to send an alert (possibly a test), we eventually expect the receiver's
+  // alert_o port to go high.
+  //
+  // This allows things like ping collisions to give us confidence that the alert gets out even when
+  // the receiver is sending ping messages.
+  //
+  // We want to disable the assertion if there is a reset or the alert complex is still
+  // initialising. We also want to disable it if there has been an injected error: the alerts that
+  // should come out in that situation rely on the ping mechanism. This injected error will either
+  // be detected with error_setreg_q or seen_skew_q.
+  //
+  // Finally, we disable it if the sender clears its alert (because ack was dropped again at the end
+  // of an alert handshake).
+  AlertCheck1_A: assert property (disable iff (!rst_ni || init_pending ||
+                                               error_setreg_q || seen_skew_q ||
+                                               i_prim_alert_sender.alert_clr)
+                                  alert_req_i || alert_test_i |=> s_eventually alert_o);
 
   // basic liveness of FSMs in case no errors are present
-  `ASSERT(FsmLivenessSender_A,
-      !error_present [*2] ##1 !error_present && !sender_is_idle |->
-      strong(##[1:$] sender_is_idle),
-      clk_i, !rst_ni || error_present || init_pending)
-  `ASSERT(FsmLivenessReceiver_A,
-      !error_present [*2] ##1 !error_present && receiver_is_idle |->
-      strong(##[1:$] receiver_is_idle),
-      clk_i, !rst_ni || error_present || init_pending)
+  FsmLivenessSender_A:
+    assert property (disable iff (!rst_ni || init_pending || error_present)
+                     s_eventually sender_is_idle);
+  FsmLivenessReceiver_A:
+    assert property (disable iff (!rst_ni || init_pending || error_present)
+                     s_eventually receiver_is_idle);
 
   // check that the in-band reset moves sender FSM into Idle state.
   `ASSERT(InBandInitFromReceiverToSender_A,
@@ -175,4 +221,29 @@ module prim_alert_rxtx_async_assert_fpv
       ##[1:30] sender_is_idle,
       clk_i, !rst_ni || error_present)
 
+  // There is a single parasitic state in the FSM of prim_alert_sender (because state_e uses 3 bits
+  // to define 7 states). The sender rather sensibly uses state_d to get back to Idle in that case
+  // as an escape route. Using a stopat to check this is fiddly because then state_d won't *have*
+  // any effect. To make this work, assert that state_d is a known state. This shows that the escape
+  // route has been wired up correctly.
+  SenderStateDValid_A: assert property (i_prim_alert_sender.state_d inside
+                                        { i_prim_alert_sender.Idle,
+                                          i_prim_alert_sender.AlertHsPhase1,
+                                          i_prim_alert_sender.AlertHsPhase2,
+                                          i_prim_alert_sender.PingHsPhase1,
+                                          i_prim_alert_sender.PingHsPhase2,
+                                          i_prim_alert_sender.Pause0,
+                                          i_prim_alert_sender.Pause1 });
+
+  // As with the previous assertion, there are two parasitic states in the FSM of
+  // prim_alert_receiver (state_e uses 3 bits to define 6 states). Again, assert that state_d is a
+  // known state.
+  ReceiverStateDValid_A: assert property (i_prim_alert_receiver.state_d inside
+                                          { i_prim_alert_receiver.Idle,
+                                            i_prim_alert_receiver.HsAckWait,
+                                            i_prim_alert_receiver.Pause0,
+                                            i_prim_alert_receiver.Pause1,
+                                            i_prim_alert_receiver.InitReq,
+                                            i_prim_alert_receiver.InitAckWait });
+
 endmodule : prim_alert_rxtx_async_assert_fpv