diff --git a/hw/formal/tools/jaspergold/fpv.tcl b/hw/formal/tools/jaspergold/fpv.tcl index 87c928e147a87..0668711ca4ed3 100644 --- a/hw/formal/tools/jaspergold/fpv.tcl +++ b/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 (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 "" + 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 } } diff --git a/hw/ip/prim/fpv/prim_alert_rxtx_async_fatal_fpv.core b/hw/ip/prim/fpv/prim_alert_rxtx_async_fatal_fpv.core index bb423db925648..d2ab734146726 100644 --- a/hw/ip/prim/fpv/prim_alert_rxtx_async_fatal_fpv.core +++ b/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 diff --git a/hw/ip/prim/fpv/prim_alert_rxtx_async_fpv.core b/hw/ip/prim/fpv/prim_alert_rxtx_async_fpv.core index 52fa7bc33f9af..6125a60394260 100644 --- a/hw/ip/prim/fpv/prim_alert_rxtx_async_fpv.core +++ b/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 diff --git a/hw/ip/prim/fpv/prim_alert_rxtx_fatal_fpv.core b/hw/ip/prim/fpv/prim_alert_rxtx_fatal_fpv.core index abb7ff0418dc9..c230606f83445 100644 --- a/hw/ip/prim/fpv/prim_alert_rxtx_fatal_fpv.core +++ b/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 diff --git a/hw/ip/prim/fpv/prim_alert_rxtx_fpv.core b/hw/ip/prim/fpv/prim_alert_rxtx_fpv.core index 415258407dd12..8252bb3a5a433 100644 --- a/hw/ip/prim/fpv/prim_alert_rxtx_fpv.core +++ b/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 diff --git a/hw/ip/prim/fpv/prim_diff_decode_fpv.core b/hw/ip/prim/fpv/prim_diff_decode_fpv.core new file mode 100644 index 0000000000000..77838f84e6d95 --- /dev/null +++ b/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 diff --git a/hw/ip/prim/fpv/tb/prim_diff_decode_bind_fpv.sv b/hw/ip/prim/fpv/tb/prim_diff_decode_bind_fpv.sv new file mode 100644 index 0000000000000..95d12b392536a --- /dev/null +++ b/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 diff --git a/hw/ip/prim/fpv/tb/rxtx_after_load.tcl b/hw/ip/prim/fpv/tb/rxtx_after_load.tcl new file mode 100644 index 0000000000000..6dd44deb928da --- /dev/null +++ b/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 diff --git a/hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert_fpv.sv b/hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert_fpv.sv index b54c58973f953..4c13a56f25f0b 100644 --- a/hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert_fpv.sv +++ b/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 diff --git a/hw/ip/prim/fpv/vip/prim_diff_decode_assert_fpv.sv b/hw/ip/prim/fpv/vip/prim_diff_decode_assert_fpv.sv new file mode 100644 index 0000000000000..9406e363b56ab --- /dev/null +++ b/hw/ip/prim/fpv/vip/prim_diff_decode_assert_fpv.sv @@ -0,0 +1,23 @@ +// Copyright lowRISC contributors (OpenTitan project). +// Licensed under the Apache License, Version 2.0, see LICENSE for details. +// SPDX-License-Identifier: Apache-2.0 +// +// Assertions that can be bound in to an instance of the prim_diff_decode module + +module prim_diff_decode_assert_fpv #( + parameter bit AsyncOn = 1'b0 +) ( + input clk_i, + input rst_ni +); + default clocking @(posedge clk_i); endclocking + default disable iff !rst_ni; + + if (AsyncOn) begin : gen_async_assertions + // There are three valid states for the FSM and we never expect it to get to the other value in + // the 2-bit encoding. + ValidState_A: assert property (gen_async.state_q inside {gen_async.IsStd, + gen_async.IsSkewing, + gen_async.SigInt}); + end +endmodule diff --git a/hw/top_earlgrey/formal/top_earlgrey_fpv_prim_cfgs.hjson b/hw/top_earlgrey/formal/top_earlgrey_fpv_prim_cfgs.hjson index fc07984b87230..4546a786296be 100644 --- a/hw/top_earlgrey/formal/top_earlgrey_fpv_prim_cfgs.hjson +++ b/hw/top_earlgrey/formal/top_earlgrey_fpv_prim_cfgs.hjson @@ -41,6 +41,7 @@ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"] rel_path: "hw/ip/prim/prim_alert_rxtx/{sub_flow}/{tool}" cov: true + after_load: ["{proj_root}/hw/ip/prim/fpv/tb/rxtx_after_load.tcl"] } { name: prim_alert_rxtx_fatal_fpv @@ -49,6 +50,7 @@ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"] rel_path: "hw/ip/prim/prim_alert_rxtx_fatal/{sub_flow}/{tool}" cov: true + after_load: ["{proj_root}/hw/ip/prim/fpv/tb/rxtx_after_load.tcl"] } { name: prim_alert_rxtx_async_fpv @@ -57,6 +59,7 @@ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"] rel_path: "hw/ip/prim/prim_alert_rxtx_async/{sub_flow}/{tool}" cov: true + after_load: ["{proj_root}/hw/ip/prim/fpv/tb/rxtx_after_load.tcl"] } { name: prim_alert_rxtx_async_fatal_fpv @@ -65,6 +68,7 @@ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"] rel_path: "hw/ip/prim/prim_alert_rxtx_fatal/{sub_flow}/{tool}" cov: true + after_load: ["{proj_root}/hw/ip/prim/fpv/tb/rxtx_after_load.tcl"] } { name: prim_arbiter_fixed_fpv