[alert_handler/fpv] Revive testbenches for esc and ping timers
This revives the FPV testbenches for the escalationa and ping timers,
and fixes / aligns several assertions with the newest code state.
Signed-off-by: Michael Schaffner <msf@google.com>
diff --git a/hw/formal/fpv_all b/hw/formal/fpv_all
index 967b73a..8184c29 100755
--- a/hw/formal/fpv_all
+++ b/hw/formal/fpv_all
@@ -55,6 +55,8 @@
"pinmux_fpv"
"rv_plic_fpv"
"rv_plic_generic_fpv"
+ "alert_handler_esc_timer_fpv"
+ "alert_handler_ping_timer_fpv"
)
#-------------------------------------------------------------------------
diff --git a/hw/ip/alert_handler/fpv/alert_handler_esc_timer_fpv.core b/hw/ip/alert_handler/fpv/alert_handler_esc_timer_fpv.core
index ac98891..be2b40c 100644
--- a/hw/ip/alert_handler/fpv/alert_handler_esc_timer_fpv.core
+++ b/hw/ip/alert_handler/fpv/alert_handler_esc_timer_fpv.core
@@ -5,7 +5,7 @@
name: "lowrisc:fpv:alert_handler_esc_timer_fpv:0.1"
description: "alert_handler_esc_timer FPV target"
filesets:
- files_fpv:
+ files_formal:
depend:
- lowrisc:prim:all
# note: this is an example config which may differ
@@ -18,10 +18,14 @@
file_type: systemVerilogSource
targets:
- default:
+ default: &default_target
# note, this setting is just used
# to generate a file list for jg
default_tool: icarus
filesets:
- - files_fpv
- toplevel: alert_handler_esc_timer_fpv
+ - files_formal
+ toplevel:
+ - alert_handler_esc_timer_fpv
+
+ formal:
+ <<: *default_target
diff --git a/hw/ip/alert_handler/fpv/alert_handler_ping_timer_fpv.core b/hw/ip/alert_handler/fpv/alert_handler_ping_timer_fpv.core
index 0bc0119..db5d846 100644
--- a/hw/ip/alert_handler/fpv/alert_handler_ping_timer_fpv.core
+++ b/hw/ip/alert_handler/fpv/alert_handler_ping_timer_fpv.core
@@ -5,7 +5,7 @@
name: "lowrisc:fpv:alert_handler_ping_timer_fpv:0.1"
description: "ALERT_HANDLER FPV target"
filesets:
- files_fpv:
+ files_formal:
depend:
- lowrisc:prim:all
# note: this is an example config which may differ
@@ -18,10 +18,14 @@
file_type: systemVerilogSource
targets:
- default:
+ default: &default_target
# note, this setting is just used
# to generate a file list for jg
default_tool: icarus
filesets:
- - files_fpv
- toplevel: alert_handler_ping_timer_fpv
+ - files_formal
+ toplevel:
+ - alert_handler_ping_timer_fpv
+
+ formal:
+ <<: *default_target
diff --git a/hw/ip/alert_handler/fpv/tb/alert_handler_esc_timer_bind_fpv.sv b/hw/ip/alert_handler/fpv/tb/alert_handler_esc_timer_bind_fpv.sv
index 30b76d9..8c57eaa 100644
--- a/hw/ip/alert_handler/fpv/tb/alert_handler_esc_timer_bind_fpv.sv
+++ b/hw/ip/alert_handler/fpv/tb/alert_handler_esc_timer_bind_fpv.sv
@@ -12,7 +12,8 @@
.rst_ni,
.en_i,
.clr_i,
- .accum_trig_i,
+ .accu_trig_i,
+ .accu_fail_i,
.timeout_en_i,
.timeout_cyc_i,
.esc_en_i,
@@ -20,7 +21,7 @@
.phase_cyc_i,
.esc_trig_o,
.esc_cnt_o,
- .esc_sig_en_o,
+ .esc_sig_req_o,
.esc_state_o
);
diff --git a/hw/ip/alert_handler/fpv/tb/alert_handler_esc_timer_fpv.sv b/hw/ip/alert_handler/fpv/tb/alert_handler_esc_timer_fpv.sv
index d15a2f3..5a94efd 100644
--- a/hw/ip/alert_handler/fpv/tb/alert_handler_esc_timer_fpv.sv
+++ b/hw/ip/alert_handler/fpv/tb/alert_handler_esc_timer_fpv.sv
@@ -10,7 +10,8 @@
input rst_ni,
input en_i,
input clr_i,
- input accum_trig_i,
+ input accu_trig_i,
+ input accu_fail_i,
input timeout_en_i,
input [EscCntDw-1:0] timeout_cyc_i,
input [N_ESC_SEV-1:0] esc_en_i,
@@ -18,7 +19,7 @@
input [N_PHASES-1:0][EscCntDw-1:0] phase_cyc_i,
output logic esc_trig_o,
output logic[EscCntDw-1:0] esc_cnt_o,
- output logic[N_ESC_SEV-1:0] esc_sig_en_o,
+ output logic[N_ESC_SEV-1:0] esc_sig_req_o,
output cstate_e esc_state_o
);
@@ -27,7 +28,8 @@
.rst_ni,
.en_i,
.clr_i,
- .accum_trig_i,
+ .accu_trig_i,
+ .accu_fail_i,
.timeout_en_i,
.timeout_cyc_i,
.esc_en_i,
@@ -35,7 +37,7 @@
.phase_cyc_i,
.esc_trig_o,
.esc_cnt_o,
- .esc_sig_en_o,
+ .esc_sig_req_o,
.esc_state_o
);
diff --git a/hw/ip/alert_handler/fpv/tb/alert_handler_ping_timer_bind_fpv.sv b/hw/ip/alert_handler/fpv/tb/alert_handler_ping_timer_bind_fpv.sv
index dbbac60..78ecf33 100644
--- a/hw/ip/alert_handler/fpv/tb/alert_handler_ping_timer_bind_fpv.sv
+++ b/hw/ip/alert_handler/fpv/tb/alert_handler_ping_timer_bind_fpv.sv
@@ -10,13 +10,15 @@
alert_handler_ping_timer_assert_fpv i_alert_handler_ping_timer_assert_fpv (
.clk_i,
.rst_ni,
- .entropy_i,
+ .edn_req_o,
+ .edn_ack_i,
+ .edn_data_i,
.en_i,
- .alert_en_i,
+ .alert_ping_en_i,
.ping_timeout_cyc_i,
.wait_cyc_mask_i,
- .alert_ping_en_o,
- .esc_ping_en_o,
+ .alert_ping_req_o,
+ .esc_ping_req_o,
.alert_ping_ok_i,
.esc_ping_ok_i,
.alert_ping_fail_o,
diff --git a/hw/ip/alert_handler/fpv/tb/alert_handler_ping_timer_fpv.sv b/hw/ip/alert_handler/fpv/tb/alert_handler_ping_timer_fpv.sv
index 47e45d5..ca18a84 100644
--- a/hw/ip/alert_handler/fpv/tb/alert_handler_ping_timer_fpv.sv
+++ b/hw/ip/alert_handler/fpv/tb/alert_handler_ping_timer_fpv.sv
@@ -8,13 +8,15 @@
module alert_handler_ping_timer_fpv import alert_pkg::*; (
input clk_i,
input rst_ni,
- input entropy_i,
+ output logic edn_req_o,
+ input edn_ack_i,
+ input [LfsrWidth-1:0] edn_data_i,
input en_i,
- input [NAlerts-1:0] alert_en_i,
+ input [NAlerts-1:0] alert_ping_en_i,
input [PING_CNT_DW-1:0] ping_timeout_cyc_i,
input [PING_CNT_DW-1:0] wait_cyc_mask_i,
- output logic [NAlerts-1:0] alert_ping_en_o,
- output logic [N_ESC_SEV-1:0] esc_ping_en_o,
+ output logic [NAlerts-1:0] alert_ping_req_o,
+ output logic [N_ESC_SEV-1:0] esc_ping_req_o,
input [NAlerts-1:0] alert_ping_ok_i,
input [N_ESC_SEV-1:0] esc_ping_ok_i,
output logic alert_ping_fail_o,
@@ -28,13 +30,15 @@
) i_alert_handler_ping_timer (
.clk_i ,
.rst_ni ,
- .entropy_i ,
+ .edn_req_o ,
+ .edn_ack_i ,
+ .edn_data_i ,
.en_i ,
- .alert_en_i ,
+ .alert_ping_en_i ,
.ping_timeout_cyc_i,
.wait_cyc_mask_i ,
- .alert_ping_en_o ,
- .esc_ping_en_o ,
+ .alert_ping_req_o ,
+ .esc_ping_req_o ,
.alert_ping_ok_i ,
.esc_ping_ok_i ,
.alert_ping_fail_o ,
diff --git a/hw/ip/alert_handler/fpv/vip/alert_handler_esc_timer_assert_fpv.sv b/hw/ip/alert_handler/fpv/vip/alert_handler_esc_timer_assert_fpv.sv
index ccedf21..b0763ff 100644
--- a/hw/ip/alert_handler/fpv/vip/alert_handler_esc_timer_assert_fpv.sv
+++ b/hw/ip/alert_handler/fpv/vip/alert_handler_esc_timer_assert_fpv.sv
@@ -12,7 +12,8 @@
input rst_ni,
input en_i,
input clr_i,
- input accum_trig_i,
+ input accu_trig_i,
+ input accu_fail_i,
input timeout_en_i,
input [EscCntDw-1:0] timeout_cyc_i,
input [N_ESC_SEV-1:0] esc_en_i,
@@ -20,7 +21,7 @@
input [N_PHASES-1:0][EscCntDw-1:0] phase_cyc_i,
input logic esc_trig_o,
input logic[EscCntDw-1:0] esc_cnt_o,
- input logic[N_ESC_SEV-1:0] esc_sig_en_o,
+ input logic[N_ESC_SEV-1:0] esc_sig_req_o,
input cstate_e esc_state_o
);
@@ -61,35 +62,46 @@
// if the class is not enabled and we are in IDLE state,
// neither of the two escalation mechanisms shall fire
`ASSERT(ClassDisabledNoEscTrig_A, esc_state_o == Idle && !en_i |-> !esc_trig_o)
- `ASSERT(ClassDisabledNoEsc_A, esc_state_o == Idle && !en_i |-> !esc_sig_en_o)
- `ASSERT(EscDisabledNoEsc_A, !esc_en_i[esc_sel] |-> !esc_sig_en_o[esc_sel])
+ `ASSERT(ClassDisabledNoEsc_A, esc_state_o == Idle && !en_i |-> !esc_sig_req_o)
+ `ASSERT(EscDisabledNoEsc_A, !esc_en_i[esc_sel] && esc_state_o != FsmError |->
+ !esc_sig_req_o[esc_sel])
// if timeout counter is enabled due to a pending interrupt, check escalation
// assume accumulation trigger is not asserted during this sequence
- `ASSERT(TimeoutEscTrig_A, ##1 en_i && $rose(timeout_en_i) && (timeout_cyc_i > 0) ##1
- timeout_en_i [*MAX_TIMEOUT_CYCLES] |=> esc_has_triggered_q,
- clk_i, !rst_ni || accum_trig_i || clr_i)
+ `ASSERT(TimeoutEscTrig_A, esc_state_o == Idle ##1 en_i && $rose(timeout_en_i) &&
+ (timeout_cyc_i > 0) ##1 timeout_en_i [*MAX_TIMEOUT_CYCLES] |=> esc_has_triggered_q,
+ clk_i, !rst_ni || accu_trig_i || clr_i || accu_fail_i)
// check whether an accum trig leads to escalation if enabled
- `ASSERT(AccumEscTrig_A, ##1 en_i && accum_trig_i && esc_state_o inside {Idle, Timeout} |=>
- esc_has_triggered_q)
+ `ASSERT(AccumEscTrig_A, ##1 en_i && accu_trig_i && esc_state_o inside {Idle, Timeout} |=>
+ esc_has_triggered_q, clk_i, !rst_ni || clr_i || accu_fail_i)
// check escalation cnt and state out
- `ASSERT(EscStateOut_A, alert_handler_esc_timer.state_q == esc_state_o)
- `ASSERT(EscCntOut_A, alert_handler_esc_timer.cnt_q == esc_cnt_o)
+ parameter logic [alert_handler_esc_timer.StateWidth-1:0] state_encodings [0:7] = '{
+ alert_handler_esc_timer.IdleSt,
+ alert_handler_esc_timer.TimeoutSt,
+ alert_handler_esc_timer.FsmErrorSt,
+ alert_handler_esc_timer.TerminalSt,
+ alert_handler_esc_timer.Phase0St,
+ alert_handler_esc_timer.Phase1St,
+ alert_handler_esc_timer.Phase2St,
+ alert_handler_esc_timer.Phase3St
+ };
+ `ASSERT(EscStateOut_A, alert_handler_esc_timer.state_q == state_encodings[esc_state_o])
+ `ASSERT(EscCntOut_A, alert_handler_esc_timer.cnt_q[0] == esc_cnt_o)
// check clr input
// we cannot use clr to exit from the timeout state
- `ASSERT(ClrCheck_A, clr_i && !(esc_state_o inside {Idle, Timeout}) |=>
+ `ASSERT(ClrCheck_A, clr_i && !(esc_state_o inside {Idle, Timeout, FsmError}) && !accu_fail_i |=>
esc_state_o == Idle)
// check escalation map
`ASSERT(PhaseEscMap_A, esc_state_o == phases[phase_sel] && esc_map_i[esc_sel] == phase_sel &&
- esc_en_i[esc_sel] |-> esc_sig_en_o[esc_sel])
+ esc_en_i[esc_sel] |-> esc_sig_req_o[esc_sel])
// check terminal state is reached eventually if triggered and not cleared
`ASSERT(TerminalState_A, esc_trig_o |-> strong(##[1:$] esc_state_o == Terminal),
- clk_i, !rst_ni || clr_i)
+ clk_i, !rst_ni || clr_i || accu_fail_i)
/////////////////////////
// Backward Assertions //
@@ -97,16 +109,18 @@
// escalation can only be triggered when in Idle or Timeout state. Trigger mechanisms are either
// the accumulation trigger or a timeout trigger
- `ASSERT(EscTrigBkwd_A, esc_trig_o |-> esc_state_o inside {Idle, Timeout} && accum_trig_i ||
- esc_state_o == Timeout && esc_cnt_o >= timeout_cyc_i)
+ `ASSERT(EscTrigBkwd_A, esc_trig_o |-> esc_state_o inside {Idle, Timeout} && accu_trig_i ||
+ esc_state_o == Timeout && esc_cnt_o >= timeout_cyc_i)
`ASSERT(NoEscTrigBkwd_A, !esc_trig_o |-> !(esc_state_o inside {Idle, Timeout}) ||
- (!en_i || !accum_trig_i || !timeout_en_i))
+ !en_i || !accu_trig_i || !timeout_en_i || clr_i)
- // escalation signals can only be asserted in the escalation phase states
- `ASSERT(EscBkwd_A, esc_sig_en_o[esc_sel] |-> esc_en_i[esc_sel] &&
- esc_has_triggered_q)
- `ASSERT(NoEscBkwd_A, !esc_sig_en_o[esc_sel] |-> !esc_en_i[esc_sel] ||
- esc_state_o != phases[esc_map_i[esc_sel]], clk_i, !rst_ni || clr_i)
+ // escalation signals can only be asserted in the escalation phase states, or
+ // if we are in the terminal FsmError state
+ `ASSERT(EscBkwd_A, esc_sig_req_o[esc_sel] |-> esc_en_i[esc_sel] &&
+ esc_has_triggered_q || esc_state_o == FsmError)
+ `ASSERT(NoEscBkwd_A, !esc_sig_req_o[esc_sel] |-> !esc_en_i[esc_sel] ||
+ esc_state_o != phases[esc_map_i[esc_sel]] && esc_state_o != FsmError,
+ clk_i, !rst_ni || clr_i)
//////////////////////
// Helper Processes //
diff --git a/hw/ip/alert_handler/fpv/vip/alert_handler_ping_timer_assert_fpv.sv b/hw/ip/alert_handler/fpv/vip/alert_handler_ping_timer_assert_fpv.sv
index 35fa43c..12651a5 100644
--- a/hw/ip/alert_handler/fpv/vip/alert_handler_ping_timer_assert_fpv.sv
+++ b/hw/ip/alert_handler/fpv/vip/alert_handler_ping_timer_assert_fpv.sv
@@ -10,13 +10,15 @@
module alert_handler_ping_timer_assert_fpv import alert_pkg::*; (
input clk_i,
input rst_ni,
- input entropy_i,
+ input edn_req_o,
+ input edn_ack_i,
+ input [LfsrWidth-1:0] edn_data_i,
input en_i,
- input [NAlerts-1:0] alert_en_i,
+ input [NAlerts-1:0] alert_ping_en_i,
input [PING_CNT_DW-1:0] ping_timeout_cyc_i,
input [PING_CNT_DW-1:0] wait_cyc_mask_i,
- input [NAlerts-1:0] alert_ping_en_o,
- input [N_ESC_SEV-1:0] esc_ping_en_o,
+ input [NAlerts-1:0] alert_ping_req_o,
+ input [N_ESC_SEV-1:0] esc_ping_req_o,
input [NAlerts-1:0] alert_ping_ok_i,
input [N_ESC_SEV-1:0] esc_ping_ok_i,
input alert_ping_fail_o,
@@ -25,8 +27,8 @@
logic [N_ESC_SEV+NAlerts-1:0] ping_en_vector, ping_en_mask, ping_ok_vector;
- assign ping_en_vector = {esc_ping_en_o, alert_ping_en_o};
- assign ping_en_mask = {N_ESC_SEV'('1), alert_en_i};
+ assign ping_en_vector = {esc_ping_req_o, alert_ping_req_o};
+ assign ping_en_mask = {N_ESC_SEV'('1), alert_ping_en_i};
assign ping_ok_vector = {esc_ping_ok_i, alert_ping_ok_i};
/////////////////
@@ -39,7 +41,7 @@
`ASSUME_FPV(PingEnSelStable_M, ##1 $stable(ping_en_sel))
// assume that the alert enable configuration is locked once en_i is high
// this is ensured by the CSR regfile on the outside
- `ASSUME_FPV(ConfigLocked0_M, en_i |-> ($stable(alert_en_i) [*]))
+ `ASSUME_FPV(ConfigLocked0_M, en_i |-> ($stable(alert_ping_en_i) [*]))
`ASSUME_FPV(ConfigLocked1_M, en_i |-> ($stable(ping_timeout_cyc_i) [*]))
// enable stays high forever, once it has been asserted
// this can be enabled in DV as well
@@ -52,10 +54,10 @@
////////////////////////
// no pings on disabled alerts
- `ASSERT(DisabledNoAlertPings_A, ((~alert_en_i) & alert_ping_en_o) == 0)
+ `ASSERT(DisabledNoAlertPings_A, ((~alert_ping_en_i) & alert_ping_req_o) == 0)
// no pings when not enabled
- `ASSERT(NoPingsWhenDisabled0_A, !en_i |-> !alert_ping_en_o)
- `ASSERT(NoPingsWhenDisabled1_A, !en_i |-> !esc_ping_en_o)
+ `ASSERT(NoPingsWhenDisabled0_A, !en_i |-> !alert_ping_req_o)
+ `ASSERT(NoPingsWhenDisabled1_A, !en_i |-> !esc_ping_req_o)
`ASSERT(NoPingsWhenDisabled2_A, en_i && !ping_en_mask[ping_en_sel] |->
!ping_en_vector[ping_en_sel])
@@ -77,8 +79,8 @@
/////////////////////////
// no pings when not enabled
- `ASSERT(NoPingsWhenDisabledBkwd0_A, alert_ping_en_o |-> en_i)
- `ASSERT(NoPingsWhenDisabledBkwd1_A, esc_ping_en_o |-> en_i)
+ `ASSERT(NoPingsWhenDisabledBkwd0_A, alert_ping_req_o |-> en_i)
+ `ASSERT(NoPingsWhenDisabledBkwd1_A, esc_ping_req_o |-> en_i)
// spurious pings (i.e. pings that where not requested)
// on alert channels
