[hw] Add default clk/rst for prim_assert macros Fixes #1259 Signed-off-by: Greg Chadwick <gac@lowrisc.org>
diff --git a/hw/ip/aes/rtl/aes.sv b/hw/ip/aes/rtl/aes.sv index b8abe6e..605bc6c 100644 --- a/hw/ip/aes/rtl/aes.sv +++ b/hw/ip/aes/rtl/aes.sv
@@ -44,7 +44,7 @@ ); // All outputs should have a known value after reset - `ASSERT_KNOWN(TlODValidKnown, tl_o.d_valid, clk_i, !rst_ni) - `ASSERT_KNOWN(TlOAReadyKnown, tl_o.a_ready, clk_i, !rst_ni) + `ASSERT_KNOWN(TlODValidKnown, tl_o.d_valid) + `ASSERT_KNOWN(TlOAReadyKnown, tl_o.a_ready) endmodule
diff --git a/hw/ip/aes/rtl/aes_control.sv b/hw/ip/aes/rtl/aes_control.sv index 8bb39af..0f31704 100644 --- a/hw/ip/aes/rtl/aes_control.sv +++ b/hw/ip/aes/rtl/aes_control.sv
@@ -383,18 +383,18 @@ assign data_out_clear_o = 1'b0; // Selectors must be known/valid - `ASSERT_KNOWN(AesModeKnown, mode_i, clk_i, !rst_ni) + `ASSERT_KNOWN(AesModeKnown, mode_i) `ASSERT(AesKeyLenValid, key_len_i inside { AES_128, AES_192, AES_256 - }, clk_i, !rst_ni) + }) `ASSERT(AesControlStateValid, aes_ctrl_cs inside { IDLE, INIT, ROUND, FINISH, CLEAR - }, clk_i, !rst_ni) + }) endmodule
diff --git a/hw/ip/aes/rtl/aes_core.sv b/hw/ip/aes/rtl/aes_core.sv index 19e1c75..f3c61e4 100644 --- a/hw/ip/aes/rtl/aes_core.sv +++ b/hw/ip/aes/rtl/aes_core.sv
@@ -410,26 +410,26 @@ //////////////// // Selectors must be known/valid - `ASSERT_KNOWN(AesModeKnown, mode_q, clk_i, !rst_ni) + `ASSERT_KNOWN(AesModeKnown, mode_q) `ASSERT(AesKeyLenValid, key_len_q inside { AES_128, AES_192, AES_256 - }, clk_i, !rst_ni) + }) `ASSERT(AesStateSelValid, state_sel inside { STATE_INIT, STATE_ROUND, STATE_CLEAR - }, clk_i, !rst_ni) + }) `ASSERT(AesAddRKSelValid, add_round_key_in_sel inside { ADD_RK_INIT, ADD_RK_ROUND, ADD_RK_FINAL - }, clk_i, !rst_ni) - `ASSERT_KNOWN(AesKeyInitSelKnown, key_init_sel, clk_i, !rst_ni) - `ASSERT_KNOWN(AesKeyFullSelKnown, key_full_sel, clk_i, !rst_ni) - `ASSERT_KNOWN(AesKeyDecSelKnown, key_dec_sel, clk_i, !rst_ni) - `ASSERT_KNOWN(AesKeyWordsSelKnown, key_words_sel, clk_i, !rst_ni) - `ASSERT_KNOWN(AesRoundKeySelKnown, round_key_sel, clk_i, !rst_ni) + }) + `ASSERT_KNOWN(AesKeyInitSelKnown, key_init_sel) + `ASSERT_KNOWN(AesKeyFullSelKnown, key_full_sel) + `ASSERT_KNOWN(AesKeyDecSelKnown, key_dec_sel) + `ASSERT_KNOWN(AesKeyWordsSelKnown, key_words_sel) + `ASSERT_KNOWN(AesRoundKeySelKnown, round_key_sel) endmodule
diff --git a/hw/ip/aes/rtl/aes_key_expand.sv b/hw/ip/aes/rtl/aes_key_expand.sv index a0af804..a57ec80 100644 --- a/hw/ip/aes/rtl/aes_key_expand.sv +++ b/hw/ip/aes/rtl/aes_key_expand.sv
@@ -330,11 +330,11 @@ assign key_o = regular; // Selectors must be known/valid - `ASSERT_KNOWN(AesModeKnown, mode_i, clk_i, !rst_ni) + `ASSERT_KNOWN(AesModeKnown, mode_i) `ASSERT(AesKeyLenValid, key_len_i inside { AES_128, AES_192, AES_256 - }, clk_i, !rst_ni) + }) endmodule
diff --git a/hw/ip/aes/rtl/aes_reg_top.sv b/hw/ip/aes/rtl/aes_reg_top.sv index c557499..6e7bdfe 100644 --- a/hw/ip/aes/rtl/aes_reg_top.sv +++ b/hw/ip/aes/rtl/aes_reg_top.sv
@@ -925,15 +925,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
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 e939e01..ccedf21 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
@@ -45,14 +45,14 @@ // Assumptions // ///////////////// - `ASSUME(TimeoutCycles_M, timeout_cyc_i < MAX_TIMEOUT_CYCLES, clk_i, !rst_ni) - `ASSUME(TimeoutCyclesConst_M, ##1 $stable(timeout_cyc_i), clk_i, !rst_ni) + `ASSUME(TimeoutCycles_M, timeout_cyc_i < MAX_TIMEOUT_CYCLES) + `ASSUME(TimeoutCyclesConst_M, ##1 $stable(timeout_cyc_i)) - `ASSUME(PhaseCycles_M, phase_cyc_i < MAX_PHASE_CYCLES, clk_i, !rst_ni) - `ASSUME(PhaseCyclesConst_M, ##1 $stable(phase_cyc_i), clk_i, !rst_ni) + `ASSUME(PhaseCycles_M, phase_cyc_i < MAX_PHASE_CYCLES) + `ASSUME(PhaseCyclesConst_M, ##1 $stable(phase_cyc_i)) - `ASSUME(EscSelConst_M, ##1 $stable(esc_sel), clk_i, !rst_ni) - `ASSUME(PhaseSelConst_M, ##1 $stable(phase_sel), clk_i, !rst_ni) + `ASSUME(EscSelConst_M, ##1 $stable(esc_sel)) + `ASSUME(PhaseSelConst_M, ##1 $stable(phase_sel)) //////////////////////// // Forward Assertions // @@ -60,9 +60,9 @@ // 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, clk_i, !rst_ni) - `ASSERT(ClassDisabledNoEsc_A, esc_state_o == Idle && !en_i |-> !esc_sig_en_o, clk_i, !rst_ni) - `ASSERT(EscDisabledNoEsc_A, !esc_en_i[esc_sel] |-> !esc_sig_en_o[esc_sel], clk_i, !rst_ni) + `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]) // if timeout counter is enabled due to a pending interrupt, check escalation // assume accumulation trigger is not asserted during this sequence @@ -72,20 +72,20 @@ // 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, clk_i, !rst_ni) + esc_has_triggered_q) // check escalation cnt and state out - `ASSERT(EscStateOut_A, alert_handler_esc_timer.state_q == esc_state_o, clk_i, !rst_ni) - `ASSERT(EscCntOut_A, alert_handler_esc_timer.cnt_q == esc_cnt_o, clk_i, !rst_ni) + `ASSERT(EscStateOut_A, alert_handler_esc_timer.state_q == esc_state_o) + `ASSERT(EscCntOut_A, alert_handler_esc_timer.cnt_q == 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}) |=> - esc_state_o == Idle, clk_i, !rst_ni) + 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], clk_i, !rst_ni) + esc_en_i[esc_sel] |-> esc_sig_en_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), @@ -98,13 +98,13 @@ // 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, clk_i, !rst_ni) + 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), clk_i, !rst_ni) + (!en_i || !accum_trig_i || !timeout_en_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, clk_i, !rst_ni) + 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)
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 397e8bc..35fa43c 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
@@ -35,64 +35,63 @@ // symbolic variable. we want to assess all valid indices int unsigned ping_en_sel; - `ASSUME_FPV(PingEnSelRange_M, ping_en_sel >= 0 && ping_en_sel < (N_ESC_SEV+NAlerts), - clk_i, !rst_ni) - `ASSUME_FPV(PingEnSelStable_M, ##1 $stable(ping_en_sel), clk_i, !rst_ni) + `ASSUME_FPV(PingEnSelRange_M, ping_en_sel >= 0 && ping_en_sel < (N_ESC_SEV+NAlerts)) + `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) [*]), clk_i, !rst_ni) - `ASSUME_FPV(ConfigLocked1_M, en_i |-> ($stable(ping_timeout_cyc_i) [*]), clk_i, !rst_ni) + `ASSUME_FPV(ConfigLocked0_M, en_i |-> ($stable(alert_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 - `ASSUME(ConfigLocked2_M, en_i |-> (##1 en_i) [*], clk_i, !rst_ni) + `ASSUME(ConfigLocked2_M, en_i |-> (##1 en_i) [*]) // reduce state space by reducing length of wait period - `ASSUME_FPV(WaitPeriod_M, wait_cyc_mask_i == 7, clk_i, !rst_ni) + `ASSUME_FPV(WaitPeriod_M, wait_cyc_mask_i == 7) //////////////////////// // Forward Assertions // //////////////////////// // no pings on disabled alerts - `ASSERT(DisabledNoAlertPings_A, ((~alert_en_i) & alert_ping_en_o) == 0, clk_i, !rst_ni) + `ASSERT(DisabledNoAlertPings_A, ((~alert_en_i) & alert_ping_en_o) == 0) // no pings when not enabled - `ASSERT(NoPingsWhenDisabled0_A, !en_i |-> !alert_ping_en_o, clk_i, !rst_ni) - `ASSERT(NoPingsWhenDisabled1_A, !en_i |-> !esc_ping_en_o, clk_i, !rst_ni) + `ASSERT(NoPingsWhenDisabled0_A, !en_i |-> !alert_ping_en_o) + `ASSERT(NoPingsWhenDisabled1_A, !en_i |-> !esc_ping_en_o) `ASSERT(NoPingsWhenDisabled2_A, en_i && !ping_en_mask[ping_en_sel] |-> - !ping_en_vector[ping_en_sel], clk_i, !rst_ni) + !ping_en_vector[ping_en_sel]) // spurious pings (i.e. pings that where not requested) // on alert channels `ASSERT(SpuriousPingsDetected0_A, en_i && !ping_en_vector[ping_en_sel] && ping_ok_vector[ping_en_sel] && ping_en_sel < NAlerts |-> - alert_ping_fail_o, clk_i, !rst_ni) + alert_ping_fail_o) // on escalation channels `ASSERT(SpuriousPingsDetected1_A, en_i && !ping_en_vector[ping_en_sel] && ping_ok_vector[ping_en_sel] && ping_en_sel >= NAlerts |-> - esc_ping_fail_o, clk_i, !rst_ni) + esc_ping_fail_o) // response must be one hot `ASSERT(SpuriousPingsDetected2_A, en_i && !$onehot0(ping_ok_vector) |-> - esc_ping_fail_o || alert_ping_fail_o, clk_i, !rst_ni) + esc_ping_fail_o || alert_ping_fail_o) ///////////////////////// // Backward Assertions // ///////////////////////// // no pings when not enabled - `ASSERT(NoPingsWhenDisabledBkwd0_A, alert_ping_en_o |-> en_i, clk_i, !rst_ni) - `ASSERT(NoPingsWhenDisabledBkwd1_A, esc_ping_en_o |-> en_i, clk_i, !rst_ni) + `ASSERT(NoPingsWhenDisabledBkwd0_A, alert_ping_en_o |-> en_i) + `ASSERT(NoPingsWhenDisabledBkwd1_A, esc_ping_en_o |-> en_i) // spurious pings (i.e. pings that where not requested) // on alert channels `ASSERT(SpuriousPingsDetectedBkwd0_A, !alert_ping_fail_o |-> !en_i || ping_en_vector[ping_en_sel] || - !ping_ok_vector[ping_en_sel] || ping_en_sel >= NAlerts, clk_i, !rst_ni) + !ping_ok_vector[ping_en_sel] || ping_en_sel >= NAlerts) // on escalation channels `ASSERT(SpuriousPingsDetectedBkwd1_A, !esc_ping_fail_o |-> !en_i || ping_en_vector[ping_en_sel] || - !ping_ok_vector[ping_en_sel] || ping_en_sel < NAlerts, clk_i, !rst_ni) + !ping_ok_vector[ping_en_sel] || ping_en_sel < NAlerts) // response must be one hot `ASSERT(SpuriousPingsDetectedBkwd2_A, !esc_ping_fail_o && !alert_ping_fail_o |-> - !en_i || $onehot0(ping_ok_vector), clk_i, !rst_ni) + !en_i || $onehot0(ping_ok_vector)) ////////////////////////////////////////////////////////// // Currently not Tested in FPV due to large state space //
diff --git a/hw/ip/alert_handler/rtl/alert_handler.sv b/hw/ip/alert_handler/rtl/alert_handler.sv index 77513ed..e9b1ca7 100644 --- a/hw/ip/alert_handler/rtl/alert_handler.sv +++ b/hw/ip/alert_handler/rtl/alert_handler.sv
@@ -203,15 +203,15 @@ //////////////// // check whether all outputs have a good known state after reset - `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid, clk_i, !rst_ni) - `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready, clk_i, !rst_ni) - `ASSERT_KNOWN(IrqAKnownO_A, intr_classa_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IrqBKnownO_A, intr_classb_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IrqCKnownO_A, intr_classc_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IrqDKnownO_A, intr_classd_o, clk_i, !rst_ni) - `ASSERT_KNOWN(CrashdumpKnownO_A, crashdump_o, clk_i, !rst_ni) - `ASSERT_KNOWN(AckPKnownO_A, alert_rx_o, clk_i, !rst_ni) - `ASSERT_KNOWN(EscPKnownO_A, esc_tx_o, clk_i, !rst_ni) + `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid) + `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready) + `ASSERT_KNOWN(IrqAKnownO_A, intr_classa_o) + `ASSERT_KNOWN(IrqBKnownO_A, intr_classb_o) + `ASSERT_KNOWN(IrqCKnownO_A, intr_classc_o) + `ASSERT_KNOWN(IrqDKnownO_A, intr_classd_o) + `ASSERT_KNOWN(CrashdumpKnownO_A, crashdump_o) + `ASSERT_KNOWN(AckPKnownO_A, alert_rx_o) + `ASSERT_KNOWN(EscPKnownO_A, esc_tx_o) // this restriction is due to specifics in the ping selection mechanism `ASSERT_INIT(CheckNAlerts, NAlerts < (256 - N_CLASSES))
diff --git a/hw/ip/alert_handler/rtl/alert_handler_accu.sv b/hw/ip/alert_handler/rtl/alert_handler_accu.sv index 9640932..d809967 100644 --- a/hw/ip/alert_handler/rtl/alert_handler_accu.sv +++ b/hw/ip/alert_handler/rtl/alert_handler_accu.sv
@@ -49,7 +49,7 @@ // Assertions // //////////////// - `ASSERT(DisabledNoTrigFwd_A, !class_en_i |-> !accu_trig_o, clk_i, !rst_ni) - `ASSERT(DisabledNoTrigBkwd_A, accu_trig_o |-> class_en_i, clk_i, !rst_ni) + `ASSERT(DisabledNoTrigFwd_A, !class_en_i |-> !accu_trig_o) + `ASSERT(DisabledNoTrigBkwd_A, accu_trig_o |-> class_en_i) endmodule : alert_handler_accu
diff --git a/hw/ip/alert_handler/rtl/alert_handler_esc_timer.sv b/hw/ip/alert_handler/rtl/alert_handler_esc_timer.sv index 435f14c..737a502 100644 --- a/hw/ip/alert_handler/rtl/alert_handler_esc_timer.sv +++ b/hw/ip/alert_handler/rtl/alert_handler_esc_timer.sv
@@ -224,15 +224,15 @@ // a clear should always bring us back to idle `ASSERT(CheckClr, clr_i && !(state_q inside {Idle, Timeout}) |=> - state_q == Idle, clk_i, !rst_ni) + state_q == Idle) // if currently in idle and not enabled, must remain here `ASSERT(CheckEn, state_q == Idle && !en_i |=> - state_q == Idle, clk_i, !rst_ni) + state_q == Idle) // Check if accumulation trigger correctly captured `ASSERT(CheckAccumTrig0, accum_trig_i && state_q == Idle && en_i |=> - state_q == Phase0, clk_i, !rst_ni) + state_q == Phase0) `ASSERT(CheckAccumTrig1, accum_trig_i && state_q == Timeout && en_i |=> - state_q == Phase0, clk_i, !rst_ni) + state_q == Phase0) // Check if timeout correctly captured `ASSERT(CheckTimeout0, state_q == Idle && timeout_en_i && en_i && timeout_cyc_i != 0 |=> state_q == Timeout, clk_i, !rst_ni || accum_trig_i) @@ -242,15 +242,15 @@ state_q == Idle, clk_i, !rst_ni || accum_trig_i) // Check if timeout correctly triggers escalation `ASSERT(CheckTimeoutTrig, state_q == Timeout && timeout_en_i && - cnt_q == timeout_cyc_i |=> state_q == Phase0, clk_i, !rst_ni) + cnt_q == timeout_cyc_i |=> state_q == Phase0) // Check whether escalation phases are correctly switched `ASSERT(CheckPhase0, state_q == Phase0 && !clr_i && cnt_q >= phase_cyc_i[0] |=> - state_q == Phase1, clk_i, !rst_ni) + state_q == Phase1) `ASSERT(CheckPhase1, state_q == Phase1 && !clr_i && cnt_q >= phase_cyc_i[1] |=> - state_q == Phase2, clk_i, !rst_ni) + state_q == Phase2) `ASSERT(CheckPhase2, state_q == Phase2 && !clr_i && cnt_q >= phase_cyc_i[2] |=> - state_q == Phase3, clk_i, !rst_ni) + state_q == Phase3) `ASSERT(CheckPhase3, state_q == Phase3 && !clr_i && cnt_q >= phase_cyc_i[3] |=> - state_q == Terminal, clk_i, !rst_ni) + state_q == Terminal) endmodule : alert_handler_esc_timer
diff --git a/hw/ip/alert_handler/rtl/alert_handler_ping_timer.sv b/hw/ip/alert_handler/rtl/alert_handler_ping_timer.sv index 1c2d43a..fc377a3 100644 --- a/hw/ip/alert_handler/rtl/alert_handler_ping_timer.sv +++ b/hw/ip/alert_handler/rtl/alert_handler_ping_timer.sv
@@ -236,9 +236,9 @@ //////////////// // internals - `ASSERT(PingOH0_A, $onehot0(ping_sel), clk_i, !rst_ni) + `ASSERT(PingOH0_A, $onehot0(ping_sel)) // we should never get into the ping state without knowing // which module to ping - `ASSERT(PingOH_A, ping_en |-> $onehot(ping_sel), clk_i, !rst_ni) + `ASSERT(PingOH_A, ping_en |-> $onehot(ping_sel)) endmodule : alert_handler_ping_timer
diff --git a/hw/ip/alert_handler/rtl/alert_handler_reg_top.sv b/hw/ip/alert_handler/rtl/alert_handler_reg_top.sv index cd7e63d..3495ca5 100644 --- a/hw/ip/alert_handler/rtl/alert_handler_reg_top.sv +++ b/hw/ip/alert_handler/rtl/alert_handler_reg_top.sv
@@ -4297,15 +4297,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/entropy_src/rtl/entropy_src_reg_pkg.sv b/hw/ip/entropy_src/rtl/entropy_src_reg_pkg.sv index 50b6296..1d692be 100644 --- a/hw/ip/entropy_src/rtl/entropy_src_reg_pkg.sv +++ b/hw/ip/entropy_src/rtl/entropy_src_reg_pkg.sv
@@ -7,7 +7,7 @@ package entropy_src_reg_pkg; // Param list - localparam int EsFifoDepth = 32; + parameter int EsFifoDepth = 32; //////////////////////////// // Typedefs for registers // @@ -148,19 +148,19 @@ } entropy_src_hw2reg_t; // Register Address - parameter ENTROPY_SRC_INTR_STATE_OFFSET = 6'h 0; - parameter ENTROPY_SRC_INTR_ENABLE_OFFSET = 6'h 4; - parameter ENTROPY_SRC_INTR_TEST_OFFSET = 6'h 8; - parameter ENTROPY_SRC_ES_REGEN_OFFSET = 6'h c; - parameter ENTROPY_SRC_ES_CONF_OFFSET = 6'h 10; - parameter ENTROPY_SRC_ES_REV_OFFSET = 6'h 14; - parameter ENTROPY_SRC_ES_ENTROPY_OFFSET = 6'h 18; - parameter ENTROPY_SRC_ES_CTRL_OFFSET = 6'h 1c; - parameter ENTROPY_SRC_ES_STATUS_OFFSET = 6'h 20; - parameter ENTROPY_SRC_ES_FDEPTHST_OFFSET = 6'h 24; - parameter ENTROPY_SRC_ES_THRESH_OFFSET = 6'h 28; - parameter ENTROPY_SRC_ES_RATE_OFFSET = 6'h 2c; - parameter ENTROPY_SRC_ES_SEED_OFFSET = 6'h 30; + parameter logic [5:0] ENTROPY_SRC_INTR_STATE_OFFSET = 6'h 0; + parameter logic [5:0] ENTROPY_SRC_INTR_ENABLE_OFFSET = 6'h 4; + parameter logic [5:0] ENTROPY_SRC_INTR_TEST_OFFSET = 6'h 8; + parameter logic [5:0] ENTROPY_SRC_ES_REGEN_OFFSET = 6'h c; + parameter logic [5:0] ENTROPY_SRC_ES_CONF_OFFSET = 6'h 10; + parameter logic [5:0] ENTROPY_SRC_ES_REV_OFFSET = 6'h 14; + parameter logic [5:0] ENTROPY_SRC_ES_ENTROPY_OFFSET = 6'h 18; + parameter logic [5:0] ENTROPY_SRC_ES_CTRL_OFFSET = 6'h 1c; + parameter logic [5:0] ENTROPY_SRC_ES_STATUS_OFFSET = 6'h 20; + parameter logic [5:0] ENTROPY_SRC_ES_FDEPTHST_OFFSET = 6'h 24; + parameter logic [5:0] ENTROPY_SRC_ES_THRESH_OFFSET = 6'h 28; + parameter logic [5:0] ENTROPY_SRC_ES_RATE_OFFSET = 6'h 2c; + parameter logic [5:0] ENTROPY_SRC_ES_SEED_OFFSET = 6'h 30; // Register Index @@ -181,7 +181,7 @@ } entropy_src_id_e; // Register width information to check illegal writes - localparam logic [3:0] ENTROPY_SRC_PERMIT [13] = '{ + parameter logic [3:0] ENTROPY_SRC_PERMIT [13] = '{ 4'b 0001, // index[ 0] ENTROPY_SRC_INTR_STATE 4'b 0001, // index[ 1] ENTROPY_SRC_INTR_ENABLE 4'b 0001, // index[ 2] ENTROPY_SRC_INTR_TEST
diff --git a/hw/ip/entropy_src/rtl/entropy_src_reg_top.sv b/hw/ip/entropy_src/rtl/entropy_src_reg_top.sv index 94e31b9..822d781 100644 --- a/hw/ip/entropy_src/rtl/entropy_src_reg_top.sv +++ b/hw/ip/entropy_src/rtl/entropy_src_reg_top.sv
@@ -23,9 +23,9 @@ import entropy_src_reg_pkg::* ; - localparam AW = 6; - localparam DW = 32; - localparam DBW = DW/8; // Byte Width + localparam int AW = 6; + localparam int DW = 32; + localparam int DBW = DW/8; // Byte Width // register signals logic reg_we; @@ -696,15 +696,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/flash_ctrl/rtl/flash_ctrl.sv b/hw/ip/flash_ctrl/rtl/flash_ctrl.sv index 771475e..de03ba6 100644 --- a/hw/ip/flash_ctrl/rtl/flash_ctrl.sv +++ b/hw/ip/flash_ctrl/rtl/flash_ctrl.sv
@@ -467,18 +467,17 @@ // Assertions - `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid, clk_i, !rst_ni) - `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready, clk_i, !rst_ni) + `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid ) + `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready ) `ASSERT_KNOWN(FlashKnownO_A, {flash_o.req, flash_o.rd, flash_o.prog, flash_o.pg_erase, - flash_o.bk_erase}, clk_i, !rst_ni) - `ASSERT_VALID_DATA(FlashAddrKnown_A, flash_o.req, flash_o.addr, clk_i, !rst_ni) - `ASSERT_VALID_DATA(FlashProgKnown_A, flash_o.prog & flash_o.req, flash_o.prog_data, - clk_i, !rst_ni) - `ASSERT_KNOWN(IntrProgEmptyKnownO_A, intr_prog_empty_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrProgLvlKnownO_A, intr_prog_lvl_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrProgRdFullKnownO_A, intr_rd_full_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrRdLvlKnownO_A, intr_rd_lvl_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrOpDoneKnownO_A, intr_op_done_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrOpErrorKnownO_A, intr_op_error_o, clk_i, !rst_ni) + flash_o.bk_erase}) + `ASSERT_VALID_DATA(FlashAddrKnown_A, flash_o.req, flash_o.addr) + `ASSERT_VALID_DATA(FlashProgKnown_A, flash_o.prog & flash_o.req, flash_o.prog_data) + `ASSERT_KNOWN(IntrProgEmptyKnownO_A, intr_prog_empty_o) + `ASSERT_KNOWN(IntrProgLvlKnownO_A, intr_prog_lvl_o ) + `ASSERT_KNOWN(IntrProgRdFullKnownO_A, intr_rd_full_o ) + `ASSERT_KNOWN(IntrRdLvlKnownO_A, intr_rd_lvl_o ) + `ASSERT_KNOWN(IntrOpDoneKnownO_A, intr_op_done_o ) + `ASSERT_KNOWN(IntrOpErrorKnownO_A, intr_op_error_o ) endmodule
diff --git a/hw/ip/flash_ctrl/rtl/flash_ctrl_reg_top.sv b/hw/ip/flash_ctrl/rtl/flash_ctrl_reg_top.sv index 56b8195..e8a4714 100644 --- a/hw/ip/flash_ctrl/rtl/flash_ctrl_reg_top.sv +++ b/hw/ip/flash_ctrl/rtl/flash_ctrl_reg_top.sv
@@ -3144,15 +3144,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/flash_ctrl/rtl/flash_mp.sv b/hw/ip/flash_ctrl/rtl/flash_mp.sv index ba51f6c..f226d8c 100644 --- a/hw/ip/flash_ctrl/rtl/flash_mp.sv +++ b/hw/ip/flash_ctrl/rtl/flash_mp.sv
@@ -134,9 +134,8 @@ // Bank erase enable should always be one-hot. We cannot erase multiple banks // at the same time - `ASSERT(bkEraseEnOnehot_a, (req_o & bk_erase_o) |-> $onehot(bk_erase_en), clk_i, !rst_ni) + `ASSERT(bkEraseEnOnehot_a, (req_o & bk_erase_o) |-> $onehot(bk_erase_en)) // Requests can only happen one at a time - `ASSERT(requestTypesOnehot_a, req_o |-> $onehot({rd_o, prog_o, pg_erase_o, bk_erase_o}), - clk_i, !rst_ni) + `ASSERT(requestTypesOnehot_a, req_o |-> $onehot({rd_o, prog_o, pg_erase_o, bk_erase_o})) endmodule // flash_erase_ctrl
diff --git a/hw/ip/gpio/rtl/gpio.sv b/hw/ip/gpio/rtl/gpio.sv index e386f78..fa6ca38 100644 --- a/hw/ip/gpio/rtl/gpio.sv +++ b/hw/ip/gpio/rtl/gpio.sv
@@ -143,8 +143,8 @@ ); // Assert Known: Outputs - `ASSERT_KNOWN(IntrGpioKnown, intr_gpio_o, clk_i, !rst_ni) - `ASSERT_KNOWN(CioGpioEnOKnown, cio_gpio_en_o, clk_i, !rst_ni) - `ASSERT_KNOWN(CioGpioOKnown, cio_gpio_o, clk_i, !rst_ni) + `ASSERT_KNOWN(IntrGpioKnown, intr_gpio_o) + `ASSERT_KNOWN(CioGpioEnOKnown, cio_gpio_en_o) + `ASSERT_KNOWN(CioGpioOKnown, cio_gpio_o) endmodule
diff --git a/hw/ip/gpio/rtl/gpio_reg_top.sv b/hw/ip/gpio/rtl/gpio_reg_top.sv index fd8bca4..0de202a 100644 --- a/hw/ip/gpio/rtl/gpio_reg_top.sv +++ b/hw/ip/gpio/rtl/gpio_reg_top.sv
@@ -706,15 +706,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/hmac/rtl/hmac.sv b/hw/ip/hmac/rtl/hmac.sv index 99c51eb..0f9734d 100644 --- a/hw/ip/hmac/rtl/hmac.sv +++ b/hw/ip/hmac/rtl/hmac.sv
@@ -523,30 +523,28 @@ // the host doesn't write data after hash_process until hash_start. // Same as "message_length shouldn't be changed between hash_process and done - `ASSERT(ValidWriteAssert, msg_fifo_req |-> !in_process, clk_i, !rst_ni) + `ASSERT(ValidWriteAssert, msg_fifo_req |-> !in_process) // `hash_process` shall be toggle and paired with `hash_start`. - `ASSERT(ValidHashStartAssert, hash_start |-> !initiated, clk_i, !rst_ni) - `ASSERT(ValidHashProcessAssert, reg_hash_process |-> initiated, clk_i, !rst_ni) + `ASSERT(ValidHashStartAssert, hash_start |-> !initiated) + `ASSERT(ValidHashProcessAssert, reg_hash_process |-> initiated) // between `hash_done` and `hash_start`, message FIFO should be empty `ASSERT(MsgFifoEmptyWhenNoOpAssert, - !in_process && !initiated |-> $stable(message_length), - clk_i, !rst_ni) + !in_process && !initiated |-> $stable(message_length)) // hmac_en should be modified only when the logic is Idle `ASSERT(ValidHmacEnConditionAssert, - hmac_en != $past(hmac_en) |-> !in_process && !initiated, - clk_i, !rst_ni) + hmac_en != $past(hmac_en) |-> !in_process && !initiated) // All outputs should be known value after reset - `ASSERT_KNOWN(IntrHmacDoneOKnown, intr_hmac_done_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrFifoFullOKnown, intr_fifo_full_o, clk_i, !rst_ni) - `ASSERT_KNOWN(TlODValidKnown, tl_o.d_valid, clk_i, !rst_ni) - `ASSERT_KNOWN(TlOAReadyKnown, tl_o.a_ready, clk_i, !rst_ni) + `ASSERT_KNOWN(IntrHmacDoneOKnown, intr_hmac_done_o) + `ASSERT_KNOWN(IntrFifoFullOKnown, intr_fifo_full_o) + `ASSERT_KNOWN(TlODValidKnown, tl_o.d_valid) + `ASSERT_KNOWN(TlOAReadyKnown, tl_o.a_ready) // Alert outputs - `ASSERT_KNOWN(AlertTxOKnown, alert_tx_o, clk_i, !rst_ni) + `ASSERT_KNOWN(AlertTxOKnown, alert_tx_o) `endif // SYNTHESIS `endif // VERILATOR
diff --git a/hw/ip/hmac/rtl/hmac_reg_top.sv b/hw/ip/hmac/rtl/hmac_reg_top.sv index 8c909be..ef1c1ed 100644 --- a/hw/ip/hmac/rtl/hmac_reg_top.sv +++ b/hw/ip/hmac/rtl/hmac_reg_top.sv
@@ -1202,15 +1202,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/hmac/rtl/sha2_pad.sv b/hw/ip/hmac/rtl/sha2_pad.sv index 9ca88e4..5ee9088 100644 --- a/hw/ip/hmac/rtl/sha2_pad.sv +++ b/hw/ip/hmac/rtl/sha2_pad.sv
@@ -311,7 +311,6 @@ // When fifo_partial, fifo shouldn't be empty and hash_process was set `ASSERT(ValidPartialConditionAssert, - fifo_partial && fifo_rvalid |-> hash_process_flag, - clk_i, !rst_ni) + fifo_partial && fifo_rvalid |-> hash_process_flag) endmodule
diff --git a/hw/ip/i2c/rtl/i2c.sv b/hw/ip/i2c/rtl/i2c.sv index 350c911..99678fa 100644 --- a/hw/ip/i2c/rtl/i2c.sv +++ b/hw/ip/i2c/rtl/i2c.sv
@@ -84,20 +84,20 @@ assign cio_scl_en_o = ~scl_int; assign cio_sda_en_o = ~sda_int; - `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid, clk_i, !rst_ni) - `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready, clk_i, !rst_ni) - `ASSERT_KNOWN(CioSclKnownO_A, cio_scl_o, clk_i, !rst_ni) - `ASSERT_KNOWN(CioSclEnKnownO_A, cio_scl_en_o, clk_i, !rst_ni) - `ASSERT_KNOWN(CioSdaKnownO_A, cio_sda_o, clk_i, !rst_ni) - `ASSERT_KNOWN(CioSdaEnKnownO_A, cio_sda_en_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrFmtWtmkKnownO_A, intr_fmt_watermark_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrRxWtmkKnownO_A, intr_rx_watermark_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrFmtOflwKnownO_A, intr_fmt_overflow_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrRxOflwKnownO_A, intr_rx_overflow_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrNakKnownO_A, intr_nak_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrSclInterfKnownO_A, intr_scl_interference_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrSdaInterfKnownO_A, intr_sda_interference_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrStretchTimeoutKnownO_A, intr_stretch_timeout_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrSdaUnstableKnownO_A, intr_sda_unstable_o, clk_i, !rst_ni) + `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid) + `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready) + `ASSERT_KNOWN(CioSclKnownO_A, cio_scl_o) + `ASSERT_KNOWN(CioSclEnKnownO_A, cio_scl_en_o) + `ASSERT_KNOWN(CioSdaKnownO_A, cio_sda_o) + `ASSERT_KNOWN(CioSdaEnKnownO_A, cio_sda_en_o) + `ASSERT_KNOWN(IntrFmtWtmkKnownO_A, intr_fmt_watermark_o) + `ASSERT_KNOWN(IntrRxWtmkKnownO_A, intr_rx_watermark_o) + `ASSERT_KNOWN(IntrFmtOflwKnownO_A, intr_fmt_overflow_o) + `ASSERT_KNOWN(IntrRxOflwKnownO_A, intr_rx_overflow_o) + `ASSERT_KNOWN(IntrNakKnownO_A, intr_nak_o) + `ASSERT_KNOWN(IntrSclInterfKnownO_A, intr_scl_interference_o) + `ASSERT_KNOWN(IntrSdaInterfKnownO_A, intr_sda_interference_o) + `ASSERT_KNOWN(IntrStretchTimeoutKnownO_A, intr_stretch_timeout_o) + `ASSERT_KNOWN(IntrSdaUnstableKnownO_A, intr_sda_unstable_o) endmodule
diff --git a/hw/ip/i2c/rtl/i2c_reg_top.sv b/hw/ip/i2c/rtl/i2c_reg_top.sv index 506f403..22c51e1 100644 --- a/hw/ip/i2c/rtl/i2c_reg_top.sv +++ b/hw/ip/i2c/rtl/i2c_reg_top.sv
@@ -2060,15 +2060,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/nmi_gen/rtl/nmi_gen_reg_top.sv b/hw/ip/nmi_gen/rtl/nmi_gen_reg_top.sv index 789527f..a717585 100644 --- a/hw/ip/nmi_gen/rtl/nmi_gen_reg_top.sv +++ b/hw/ip/nmi_gen/rtl/nmi_gen_reg_top.sv
@@ -467,15 +467,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/padctrl/fpv/vip/padctrl_assert_fpv.sv b/hw/ip/padctrl/fpv/vip/padctrl_assert_fpv.sv index aff804a..9bb44f5 100644 --- a/hw/ip/padctrl/fpv/vip/padctrl_assert_fpv.sv +++ b/hw/ip/padctrl/fpv/vip/padctrl_assert_fpv.sv
@@ -42,19 +42,15 @@ if (Impl == ImplGeneric) begin : gen_mio_generic `ASSERT(MioWarl_A, padctrl.reg2hw.mio_pads[mio_sel].qe |=> - !(|mio_attr_o[mio_sel][padctrl_reg_pkg::AttrDw-1:6]), - clk_i, !rst_ni) + !(|mio_attr_o[mio_sel][padctrl_reg_pkg::AttrDw-1:6])) `ASSERT(MioAttr_A, padctrl.reg2hw.mio_pads[mio_sel].qe |=> - mio_attr_o[mio_sel][5:0] == $past(padctrl.reg2hw.mio_pads[mio_sel].q[5:0]), - clk_i, !rst_ni) + mio_attr_o[mio_sel][5:0] == $past(padctrl.reg2hw.mio_pads[mio_sel].q[5:0])) end else if (Impl == ImplXilinx) begin : gen_mio_xilinx `ASSERT(MioWarl_A, padctrl.reg2hw.mio_pads[mio_sel].qe |=> - !(|padctrl.mio_attr_q[mio_sel][padctrl_reg_pkg::AttrDw-1:2]), - clk_i, !rst_ni) + !(|padctrl.mio_attr_q[mio_sel][padctrl_reg_pkg::AttrDw-1:2])) `ASSERT(MioAttr_A, padctrl.reg2hw.mio_pads[mio_sel].qe |=> mio_attr_o[mio_sel][1:0] == - $past(padctrl.reg2hw.mio_pads[mio_sel].q[1:0]), - clk_i, !rst_ni) + $past(padctrl.reg2hw.mio_pads[mio_sel].q[1:0])) end else begin : gen_mio_failure `ASSERT_INIT(UnknownImpl_A, 0) end @@ -67,19 +63,15 @@ `ASSUME(NDioStable_M, ##1 $stable(dio_sel), clk_i, !rst_ni) if (Impl == ImplGeneric) begin : gen_dio_generic `ASSERT(DioWarl_A, padctrl.reg2hw.dio_pads[dio_sel].qe |=> - !(|dio_attr_o[dio_sel][padctrl_reg_pkg::AttrDw-1:6]), - clk_i, !rst_ni) + !(|dio_attr_o[dio_sel][padctrl_reg_pkg::AttrDw-1:6])) `ASSERT(DioAttr_A, padctrl.reg2hw.dio_pads[dio_sel].qe |=> - dio_attr_o[dio_sel][5:0] == $past(padctrl.reg2hw.dio_pads[dio_sel].q[5:0]), - clk_i, !rst_ni) + dio_attr_o[dio_sel][5:0] == $past(padctrl.reg2hw.dio_pads[dio_sel].q[5:0])) end else if (Impl == ImplXilinx) begin : gen_dio_xilinx `ASSERT(DioWarl_A, padctrl.reg2hw.dio_pads[dio_sel].qe |=> - !(|padctrl.dio_attr_q[dio_sel][5:2]), - clk_i, !rst_ni) + !(|padctrl.dio_attr_q[dio_sel][5:2])) `ASSERT(DioAttr_A, padctrl.reg2hw.dio_pads[dio_sel].qe |=> dio_attr_o[dio_sel][1:0] == - $past(padctrl.reg2hw.dio_pads[dio_sel].q[1:0]), - clk_i, !rst_ni) + $past(padctrl.reg2hw.dio_pads[dio_sel].q[1:0])) end else begin : gen_dio_failure `ASSERT_INIT(UnknownImpl_A, 0) end
diff --git a/hw/ip/padctrl/rtl/padctrl.sv b/hw/ip/padctrl/rtl/padctrl.sv index 22d90fd..e35dcca 100644 --- a/hw/ip/padctrl/rtl/padctrl.sv +++ b/hw/ip/padctrl/rtl/padctrl.sv
@@ -113,9 +113,9 @@ // Assertions // //////////////// - `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid, clk_i, !rst_ni) - `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready, clk_i, !rst_ni) - `ASSERT_KNOWN(MioKnownO_A, mio_attr_o, clk_i, !rst_ni) - `ASSERT_KNOWN(DioKnownO_A, dio_attr_o, clk_i, !rst_ni) + `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid) + `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready) + `ASSERT_KNOWN(MioKnownO_A, mio_attr_o) + `ASSERT_KNOWN(DioKnownO_A, dio_attr_o) endmodule : padctrl
diff --git a/hw/ip/padctrl/rtl/padctrl_reg_top.sv b/hw/ip/padctrl/rtl/padctrl_reg_top.sv index f615013..0ff448a 100644 --- a/hw/ip/padctrl/rtl/padctrl_reg_top.sv +++ b/hw/ip/padctrl/rtl/padctrl_reg_top.sv
@@ -681,15 +681,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/pinmux/fpv/vip/pinmux_assert_fpv.sv b/hw/ip/pinmux/fpv/vip/pinmux_assert_fpv.sv index 3f707e2..9cc2894 100644 --- a/hw/ip/pinmux/fpv/vip/pinmux_assert_fpv.sv +++ b/hw/ip/pinmux/fpv/vip/pinmux_assert_fpv.sv
@@ -32,11 +32,11 @@ assign periph_insel = pinmux.reg2hw.periph_insel[periph_sel_i]; `ASSERT(InSel0_A, periph_insel.q == 0 |-> - mio_to_periph_o[periph_sel_i] == 1'b0, clk_i, !rst_ni) + mio_to_periph_o[periph_sel_i] == 1'b0) `ASSERT(InSel1_A, periph_insel.q == 1 |-> - mio_to_periph_o[periph_sel_i] == 1'b1, clk_i, !rst_ni) + mio_to_periph_o[periph_sel_i] == 1'b1) `ASSERT(InSelN_A, periph_insel.q > 1 |-> - mio_to_periph_o[periph_sel_i] == mio_in_i[periph_insel.q - 2], clk_i, !rst_ni) + mio_to_periph_o[periph_sel_i] == mio_in_i[periph_insel.q - 2]) //////////////// // Output Mux // @@ -48,20 +48,20 @@ assign mio_outsel = pinmux.reg2hw.mio_outsel[mio_sel_i]; `ASSERT(OutSel0_A, mio_outsel.q == 0 |-> - mio_out_o[mio_sel_i] == 1'b0, clk_i, !rst_ni) + mio_out_o[mio_sel_i] == 1'b0) `ASSERT(OutSel1_A, mio_outsel.q == 1 |-> - mio_out_o[mio_sel_i] == 1'b1, clk_i, !rst_ni) + mio_out_o[mio_sel_i] == 1'b1) `ASSERT(OutSel2_A, mio_outsel.q == 2 |-> - mio_out_o[mio_sel_i] == 1'b0, clk_i, !rst_ni) + mio_out_o[mio_sel_i] == 1'b0) `ASSERT(OutSelN_A, mio_outsel.q > 2 |-> - mio_out_o[mio_sel_i] == periph_to_mio_i[mio_outsel.q - 3], clk_i, !rst_ni) + mio_out_o[mio_sel_i] == periph_to_mio_i[mio_outsel.q - 3]) `ASSERT(OutSelOe0_A, mio_outsel.q == 0 |-> - mio_oe_o[mio_sel_i] == 1'b1, clk_i, !rst_ni) + mio_oe_o[mio_sel_i] == 1'b1) `ASSERT(OutSelOe1_A, mio_outsel.q == 1 |-> - mio_oe_o[mio_sel_i] == 1'b1, clk_i, !rst_ni) + mio_oe_o[mio_sel_i] == 1'b1) `ASSERT(OutSelOe2_A, mio_outsel.q == 2 |-> - mio_oe_o[mio_sel_i] == 1'b0, clk_i, !rst_ni) + mio_oe_o[mio_sel_i] == 1'b0) `ASSERT(OutSelOeN_A, mio_outsel.q > 2 |-> - mio_oe_o[mio_sel_i] == periph_to_mio_oe_i[mio_outsel.q - 3], clk_i, !rst_ni) + mio_oe_o[mio_sel_i] == periph_to_mio_oe_i[mio_outsel.q - 3]) endmodule : pinmux_assert_fpv
diff --git a/hw/ip/pinmux/fpv/vip/pinmux_csr_assert_fpv.sv b/hw/ip/pinmux/fpv/vip/pinmux_csr_assert_fpv.sv index c9b2960..6e54c7b 100644 --- a/hw/ip/pinmux/fpv/vip/pinmux_csr_assert_fpv.sv +++ b/hw/ip/pinmux/fpv/vip/pinmux_csr_assert_fpv.sv
@@ -77,8 +77,8 @@ // for all the regsters, declare assertion // read/write assertions for register: regen - `ASSERT(regen_wr_A, wr_P(0, 5'h0, i_pinmux.i_reg_top.regen_we, 0), clk_i, !rst_ni) - `ASSERT(regen_rd_A, rd_P(0, 5'h0, i_pinmux.i_reg_top.regen_qs), clk_i, !rst_ni) + `ASSERT(regen_wr_A, wr_P(0, 5'h0, i_pinmux.i_reg_top.regen_we, 0)) + `ASSERT(regen_rd_A, rd_P(0, 5'h0, i_pinmux.i_reg_top.regen_qs)) // define local fpv variable for the multi_reg logic [63:0] periph_insel_q_fpv; @@ -87,14 +87,14 @@ end // read/write assertions for register: periph_insel0 - `ASSERT(periph_insel0_wr_A, wr_P(31, 5'h4, periph_insel_q_fpv[31:0], i_pinmux.i_reg_top.regen_qs), clk_i, !rst_ni) - `ASSERT(periph_insel0_stable_A, wr_regen_stable_P(i_pinmux.i_reg_top.regen_qs, periph_insel_q_fpv[31:0]), clk_i, !rst_ni) - `ASSERT(periph_insel0_rd_A, rd_P(31, 5'h4, periph_insel_q_fpv[31:0]), clk_i, !rst_ni) + `ASSERT(periph_insel0_wr_A, wr_P(31, 5'h4, periph_insel_q_fpv[31:0], i_pinmux.i_reg_top.regen_qs)) + `ASSERT(periph_insel0_stable_A, wr_regen_stable_P(i_pinmux.i_reg_top.regen_qs, periph_insel_q_fpv[31:0])) + `ASSERT(periph_insel0_rd_A, rd_P(31, 5'h4, periph_insel_q_fpv[31:0])) // read/write assertions for register: periph_insel1 - `ASSERT(periph_insel1_wr_A, wr_P(31, 5'h8, periph_insel_q_fpv[63:32], i_pinmux.i_reg_top.regen_qs), clk_i, !rst_ni) - `ASSERT(periph_insel1_stable_A, wr_regen_stable_P(i_pinmux.i_reg_top.regen_qs, periph_insel_q_fpv[63:32]), clk_i, !rst_ni) - `ASSERT(periph_insel1_rd_A, rd_P(31, 5'h8, periph_insel_q_fpv[63:32]), clk_i, !rst_ni) + `ASSERT(periph_insel1_wr_A, wr_P(31, 5'h8, periph_insel_q_fpv[63:32], i_pinmux.i_reg_top.regen_qs)) + `ASSERT(periph_insel1_stable_A, wr_regen_stable_P(i_pinmux.i_reg_top.regen_qs, periph_insel_q_fpv[63:32])) + `ASSERT(periph_insel1_rd_A, rd_P(31, 5'h8, periph_insel_q_fpv[63:32])) // define local fpv variable for the multi_reg logic [39:0] mio_outsel_q_fpv; @@ -103,13 +103,13 @@ end // read/write assertions for register: mio_outsel0 - `ASSERT(mio_outsel0_wr_A, wr_P(29, 5'hc, mio_outsel_q_fpv[29:0], i_pinmux.i_reg_top.regen_qs), clk_i, !rst_ni) - `ASSERT(mio_outsel0_stable_A, wr_regen_stable_P(i_pinmux.i_reg_top.regen_qs, mio_outsel_q_fpv[29:0]), clk_i, !rst_ni) - `ASSERT(mio_outsel0_rd_A, rd_P(29, 5'hc, mio_outsel_q_fpv[29:0]), clk_i, !rst_ni) + `ASSERT(mio_outsel0_wr_A, wr_P(29, 5'hc, mio_outsel_q_fpv[29:0], i_pinmux.i_reg_top.regen_qs)) + `ASSERT(mio_outsel0_stable_A, wr_regen_stable_P(i_pinmux.i_reg_top.regen_qs, mio_outsel_q_fpv[29:0])) + `ASSERT(mio_outsel0_rd_A, rd_P(29, 5'hc, mio_outsel_q_fpv[29:0])) // read/write assertions for register: mio_outsel1 - `ASSERT(mio_outsel1_wr_A, wr_P(9, 5'h10, mio_outsel_q_fpv[39:30], i_pinmux.i_reg_top.regen_qs), clk_i, !rst_ni) - `ASSERT(mio_outsel1_stable_A, wr_regen_stable_P(i_pinmux.i_reg_top.regen_qs, mio_outsel_q_fpv[39:30]), clk_i, !rst_ni) - `ASSERT(mio_outsel1_rd_A, rd_P(9, 5'h10, mio_outsel_q_fpv[39:30]), clk_i, !rst_ni) + `ASSERT(mio_outsel1_wr_A, wr_P(9, 5'h10, mio_outsel_q_fpv[39:30], i_pinmux.i_reg_top.regen_qs)) + `ASSERT(mio_outsel1_stable_A, wr_regen_stable_P(i_pinmux.i_reg_top.regen_qs, mio_outsel_q_fpv[39:30])) + `ASSERT(mio_outsel1_rd_A, rd_P(9, 5'h10, mio_outsel_q_fpv[39:30])) endmodule
diff --git a/hw/ip/pinmux/rtl/pinmux.sv b/hw/ip/pinmux/rtl/pinmux.sv index ace93c3..25769bb 100644 --- a/hw/ip/pinmux/rtl/pinmux.sv +++ b/hw/ip/pinmux/rtl/pinmux.sv
@@ -74,10 +74,10 @@ // Assertions // //////////////// - `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid, clk_i, !rst_ni) - `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready, clk_i, !rst_ni) - `ASSERT_KNOWN(MioToPeriphKnownO_A, mio_to_periph_o, clk_i, !rst_ni) - `ASSERT_KNOWN(MioOutKnownO_A, mio_out_o, clk_i, !rst_ni) - `ASSERT_KNOWN(MioOeKnownO_A, mio_oe_o, clk_i, !rst_ni) + `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid) + `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready) + `ASSERT_KNOWN(MioToPeriphKnownO_A, mio_to_periph_o) + `ASSERT_KNOWN(MioOutKnownO_A, mio_out_o) + `ASSERT_KNOWN(MioOeKnownO_A, mio_oe_o) endmodule : pinmux
diff --git a/hw/ip/pinmux/rtl/pinmux_reg_top.sv b/hw/ip/pinmux/rtl/pinmux_reg_top.sv index df8359b..3926c0d 100644 --- a/hw/ip/pinmux/rtl/pinmux_reg_top.sv +++ b/hw/ip/pinmux/rtl/pinmux_reg_top.sv
@@ -964,15 +964,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
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 2085d46..5f4b3df 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
@@ -50,9 +50,9 @@ end // Note: we can only detect sigint errors where one wire is flipped. - `ASSUME_FPV(PingErrorsAreOH_M, $onehot0({ping_err_pi, ping_err_ni}), clk_i, !rst_ni) - `ASSUME_FPV(AckErrorsAreOH_M, $onehot0({ack_err_pi, ack_err_ni}), clk_i, !rst_ni) - `ASSUME_FPV(AlertErrorsAreOH_M, $onehot0({alert_err_pi, alert_err_ni}), clk_i, !rst_ni) + `ASSUME_FPV(PingErrorsAreOH_M, $onehot0({ping_err_pi, ping_err_ni}) ) + `ASSUME_FPV(AckErrorsAreOH_M, $onehot0({ack_err_pi, ack_err_ni}) ) + `ASSUME_FPV(AlertErrorsAreOH_M, $onehot0({alert_err_pi, alert_err_ni})) // ping will stay high until ping ok received, then it must be deasserted // TODO: this excludes the case where no ping ok will be returned due to an error
diff --git a/hw/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv b/hw/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv index 5cea725..4f55520 100644 --- a/hw/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv +++ b/hw/ip/prim/fpv/vip/prim_esc_rxtx_assert_fpv.sv
@@ -36,8 +36,8 @@ // assume that the ping enable and escalation enable signals will eventually be deasserted (and // esc will stay low for more than 2 cycles) - `ASSUME_FPV(FiniteEsc_M, esc_en_i |-> strong(##[1:$] !esc_en_i [*2]), clk_i, !rst_ni) - `ASSUME_FPV(FinitePing_M, ping_en_i |-> strong(##[1:$] !ping_en_i), clk_i, !rst_ni) + `ASSUME_FPV(FiniteEsc_M, esc_en_i |-> strong(##[1:$] !esc_en_i [*2])) + `ASSUME_FPV(FinitePing_M, ping_en_i |-> strong(##[1:$] !ping_en_i)) // ping response mus occur within 4 cycles (given that no // error occured within the previous cycles) @@ -53,9 +53,9 @@ // check that a single error on the diffpairs is detected `ASSERT(SingleSigIntDetected0_A, {esc_err_pi, esc_err_ni} == '0 ##1 - $onehot({resp_err_pi, resp_err_ni}) |-> integ_fail_o, clk_i, !rst_ni) + $onehot({resp_err_pi, resp_err_ni}) |-> integ_fail_o) `ASSERT(SingleSigIntDetected1_A, $onehot({esc_err_pi, esc_err_ni}) ##1 - {resp_err_pi, resp_err_ni} == '0 |-> integ_fail_o, clk_i, !rst_ni) + {resp_err_pi, resp_err_ni} == '0 |-> integ_fail_o) // basic liveness of FSMs in case no errors are present `ASSERT(FsmLivenessSender_A, (prim_esc_rxtx_fpv.i_prim_esc_sender.state_q !=
diff --git a/hw/ip/prim/fpv/vip/prim_fifo_sync_assert_fpv.sv b/hw/ip/prim/fpv/vip/prim_fifo_sync_assert_fpv.sv index f0a13f6..9090e4c 100644 --- a/hw/ip/prim/fpv/vip/prim_fifo_sync_assert_fpv.sv +++ b/hw/ip/prim/fpv/vip/prim_fifo_sync_assert_fpv.sv
@@ -126,9 +126,9 @@ end // check the data - `ASSERT(DataCheck_A, rvalid |-> rdata == ref_rdata, clk_i, !rst_ni) + `ASSERT(DataCheck_A, rvalid |-> rdata == ref_rdata) // check the depth - `ASSERT(DepthCheck_A, ref_depth == depth, clk_i, !rst_ni) + `ASSERT(DepthCheck_A, ref_depth == depth) end @@ -137,9 +137,9 @@ //////////////////////// // assert depth of FIFO - `ASSERT(Depth_A, depth <= Depth, clk_i, !rst_ni) + `ASSERT(Depth_A, depth <= Depth) // if we clear the FIFO, it must be empty in the next cycle - `ASSERT(CheckClrDepth_A, clr_i |=> depth == 0, clk_i, !rst_ni) + `ASSERT(CheckClrDepth_A, clr_i |=> depth == 0) // check write on full `ASSERT(WriteFull_A, depth == Depth && wvalid && !rready |=> depth == $past(depth), clk_i, !rst_ni || clr_i) @@ -158,21 +158,20 @@ // if there is no register, the FIFO is per definition pass-through `ASSERT_INIT(ZeroDepthNeedsPass_A, Pass == 1) // depth must remain zero - `ASSERT(DepthAlwaysZero_A, depth == 0, clk_i, !rst_ni) + `ASSERT(DepthAlwaysZero_A, depth == 0) // data is just passed through - `ASSERT(DataPassThru_A, wdata == rdata, clk_i, !rst_ni) + `ASSERT(DataPassThru_A, wdata == rdata) // FIFO is ready if downstream logic is ready - `ASSERT(Wready_A, rready == wready, clk_i, !rst_ni) + `ASSERT(Wready_A, rready == wready) // valid input is valid output - `ASSERT(Rvalid_A, rvalid == wvalid, clk_i, !rst_ni) + `ASSERT(Rvalid_A, rvalid == wvalid) // ensure full coverage - `ASSERT(UnusedClr_A, prim_fifo_sync.gen_passthru_fifo.unused_clr == clr_i, - clk_i, !rst_ni) + `ASSERT(UnusedClr_A, prim_fifo_sync.gen_passthru_fifo.unused_clr == clr_i) end else begin : gen_depth_gt0 // check wready - `ASSERT(Wready_A, depth < Depth |-> wready, clk_i, !rst_ni) + `ASSERT(Wready_A, depth < Depth |-> wready) // check rvalid - `ASSERT(Rvalid_A, depth > 0 |-> rvalid, clk_i, !rst_ni) + `ASSERT(Rvalid_A, depth > 0 |-> rvalid) // check write only `ASSERT(WriteOnly_A, wvalid && wready && !rready && depth < Depth |=> depth == $past(depth) + 1, clk_i, !rst_ni || clr_i) @@ -184,10 +183,10 @@ if (Pass) begin : gen_pass_fwd // if we clear the FIFO, it must be empty in the next cycle // but we may also get a pass through - `ASSERT(CheckClrValid_A, clr_i |=> wvalid == rvalid, clk_i, !rst_ni) + `ASSERT(CheckClrValid_A, clr_i |=> wvalid == rvalid) end else begin : gen_nopass_fwd // if we clear the FIFO, it must be empty in the next cycle - `ASSERT(CheckClrValid_A, clr_i |=> !rvalid, clk_i, !rst_ni) + `ASSERT(CheckClrValid_A, clr_i |=> !rvalid) end ///////////////////////// @@ -196,19 +195,19 @@ if (Pass) begin : gen_pass_bkwd // there is still space in the FIFO or downstream logic is ready - `ASSERT(WreadySpacekBkwd_A, wready |-> depth < Depth || rready, clk_i, !rst_ni) + `ASSERT(WreadySpacekBkwd_A, wready |-> depth < Depth || rready) // elements ready to be read or upstream data is valid - `ASSERT(RvalidElemskBkwd_A, rvalid |-> depth > 0 || wvalid, clk_i, !rst_ni) + `ASSERT(RvalidElemskBkwd_A, rvalid |-> depth > 0 || wvalid) end else begin : gen_nopass_bkwd // there is still space in the FIFO - `ASSERT(WreadySpacekBkwd_A, wready |-> depth < Depth, clk_i, !rst_ni) + `ASSERT(WreadySpacekBkwd_A, wready |-> depth < Depth) // elements ready to be read - `ASSERT(RvalidElemskBkwd_A, rvalid |-> depth > 0, clk_i, !rst_ni) + `ASSERT(RvalidElemskBkwd_A, rvalid |-> depth > 0) end // no more space in the FIFO - `ASSERT(WreadyNoSpaceBkwd_A, !wready |-> depth == Depth, clk_i, !rst_ni) + `ASSERT(WreadyNoSpaceBkwd_A, !wready |-> depth == Depth) // elements ready to be read - `ASSERT(RvalidNoElemskBkwd_A, !rvalid |-> depth == 0, clk_i, !rst_ni) + `ASSERT(RvalidNoElemskBkwd_A, !rvalid |-> depth == 0) endmodule : prim_fifo_sync_assert_fpv
diff --git a/hw/ip/prim/rtl/prim_alert_receiver.sv b/hw/ip/prim/rtl/prim_alert_receiver.sv index 04d9deb..7f9b3e4 100644 --- a/hw/ip/prim/rtl/prim_alert_receiver.sv +++ b/hw/ip/prim/rtl/prim_alert_receiver.sv
@@ -171,25 +171,25 @@ //////////////// // check whether all outputs have a good known state after reset - `ASSERT_KNOWN(PingOkKnownO_A, ping_ok_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntegFailKnownO_A, integ_fail_o, clk_i, !rst_ni) - `ASSERT_KNOWN(AlertKnownO_A, alert_o, clk_i, !rst_ni) - `ASSERT_KNOWN(PingPKnownO_A, alert_rx_o, clk_i, !rst_ni) + `ASSERT_KNOWN(PingOkKnownO_A, ping_ok_o) + `ASSERT_KNOWN(IntegFailKnownO_A, integ_fail_o) + `ASSERT_KNOWN(AlertKnownO_A, alert_o) + `ASSERT_KNOWN(PingPKnownO_A, alert_rx_o) // check encoding of outgoing diffpairs - `ASSERT(PingDiffOk_A, alert_rx_o.ping_p ^ alert_rx_o.ping_n, clk_i, !rst_ni) - `ASSERT(AckDiffOk_A, alert_rx_o.ack_p ^ alert_rx_o.ack_n, clk_i, !rst_ni) + `ASSERT(PingDiffOk_A, alert_rx_o.ping_p ^ alert_rx_o.ping_n) + `ASSERT(AckDiffOk_A, alert_rx_o.ack_p ^ alert_rx_o.ack_n) // ping request at input -> need to see encoded ping request - `ASSERT(PingRequest0_A, ##1 $rose(ping_en_i) |=> $changed(alert_rx_o.ping_p), clk_i, !rst_ni) + `ASSERT(PingRequest0_A, ##1 $rose(ping_en_i) |=> $changed(alert_rx_o.ping_p)) // ping response implies it has been requested - `ASSERT(PingResponse0_A, ping_ok_o |-> ping_pending_q, clk_i, !rst_ni) + `ASSERT(PingResponse0_A, ping_ok_o |-> ping_pending_q) // correctly latch ping request - `ASSERT(PingPending_A, ##1 $rose(ping_en_i) |=> ping_pending_q, clk_i, !rst_ni) + `ASSERT(PingPending_A, ##1 $rose(ping_en_i) |=> ping_pending_q) if (AsyncOn) begin : gen_async_assert // signal integrity check propagation `ASSERT(SigInt_A, alert_tx_i.alert_p == alert_tx_i.alert_n [*2] |-> - ##2 integ_fail_o, clk_i, !rst_ni) + ##2 integ_fail_o) // TODO: need to add skewed cases as well, the assertions below assume no skew at the moment // ping response `ASSERT(PingResponse1_A, ##1 $rose(alert_tx_i.alert_p) && @@ -200,7 +200,7 @@ state_q == Idle && !ping_pending_q |-> alert_o, clk_i, !rst_ni || integ_fail_o) end else begin : gen_sync_assert // signal integrity check propagation - `ASSERT(SigInt_A, alert_tx_i.alert_p == alert_tx_i.alert_n |-> integ_fail_o, clk_i, !rst_ni) + `ASSERT(SigInt_A, alert_tx_i.alert_p == alert_tx_i.alert_n |-> integ_fail_o) // ping response `ASSERT(PingResponse1_A, ##1 $rose(alert_tx_i.alert_p) && state_q == Idle && ping_pending_q |-> ping_ok_o, clk_i, !rst_ni || integ_fail_o)
diff --git a/hw/ip/prim/rtl/prim_alert_sender.sv b/hw/ip/prim/rtl/prim_alert_sender.sv index fc7a1b9..1efc71e 100644 --- a/hw/ip/prim/rtl/prim_alert_sender.sv +++ b/hw/ip/prim/rtl/prim_alert_sender.sv
@@ -191,18 +191,18 @@ //////////////// // check whether all outputs have a good known state after reset - `ASSERT_KNOWN(AlertPKnownO_A, alert_tx_o, clk_i, !rst_ni) + `ASSERT_KNOWN(AlertPKnownO_A, alert_tx_o) if (AsyncOn) begin : gen_async_assert // check propagation of sigint issues to output within three cycles `ASSERT(SigIntPing_A, alert_rx_i.ping_p == alert_rx_i.ping_n [*2] |-> - ##3 alert_tx_o.alert_p == alert_tx_o.alert_n, clk_i, !rst_ni) + ##3 alert_tx_o.alert_p == alert_tx_o.alert_n) `ASSERT(SigIntAck_A, alert_rx_i.ack_p == alert_rx_i.ack_n [*2] |-> - ##3 alert_tx_o.alert_p == alert_tx_o.alert_n, clk_i, !rst_ni) + ##3 alert_tx_o.alert_p == alert_tx_o.alert_n) // output must be driven diff unless sigint issue detected `ASSERT(DiffEncoding_A, (alert_rx_i.ack_p ^ alert_rx_i.ack_n) && (alert_rx_i.ping_p ^ alert_rx_i.ping_n) |-> - ##3 alert_tx_o.alert_p ^ alert_tx_o.alert_n, clk_i, !rst_ni) + ##3 alert_tx_o.alert_p ^ alert_tx_o.alert_n) // handshakes can take indefinite time if blocked due to sigint on outgoing // lines (which is not visible here). thus, we only check whether the @@ -214,13 +214,12 @@ end else begin : gen_sync_assert // check propagation of sigint issues to output within one cycle `ASSERT(SigIntPing_A, alert_rx_i.ping_p == alert_rx_i.ping_n |=> - alert_tx_o.alert_p == alert_tx_o.alert_n, clk_i, !rst_ni) + alert_tx_o.alert_p == alert_tx_o.alert_n) `ASSERT(SigIntAck_A, alert_rx_i.ack_p == alert_rx_i.ack_n |=> - alert_tx_o.alert_p == alert_tx_o.alert_n, clk_i, !rst_ni) + alert_tx_o.alert_p == alert_tx_o.alert_n) // output must be driven diff unless sigint issue detected `ASSERT(DiffEncoding_A, (alert_rx_i.ack_p ^ alert_rx_i.ack_n) && - (alert_rx_i.ping_p ^ alert_rx_i.ping_n) |=> alert_tx_o.alert_p ^ alert_tx_o.alert_n, - clk_i, !rst_ni) + (alert_rx_i.ping_p ^ alert_rx_i.ping_n) |=> alert_tx_o.alert_p ^ alert_tx_o.alert_n) // handshakes can take indefinite time if blocked due to sigint on outgoing // lines (which is not visible here). thus, we only check whether the handshake // is correctly initiated and defer the full handshake checking to the testbench.
diff --git a/hw/ip/prim/rtl/prim_arbiter_ppc.sv b/hw/ip/prim/rtl/prim_arbiter_ppc.sv index c59f943..5f657b9 100644 --- a/hw/ip/prim/rtl/prim_arbiter_ppc.sv +++ b/hw/ip/prim/rtl/prim_arbiter_ppc.sv
@@ -107,41 +107,41 @@ //////////////// // we can only grant one requestor at a time - `ASSERT(CheckHotOne_A, $onehot0(gnt_o), clk_i, !rst_ni) + `ASSERT(CheckHotOne_A, $onehot0(gnt_o)) // A grant implies that the sink is ready - `ASSERT(GntImpliesReady_A, |gnt_o |-> ready_i, clk_i, !rst_ni) + `ASSERT(GntImpliesReady_A, |gnt_o |-> ready_i) // A grant implies that the arbiter asserts valid as well - `ASSERT(GntImpliesValid_A, |gnt_o |-> valid_o, clk_i, !rst_ni) + `ASSERT(GntImpliesValid_A, |gnt_o |-> valid_o) // A request and a sink that is ready imply a grant - `ASSERT(ReqAndReadyImplyGrant_A, |req_i && ready_i |-> |gnt_o, clk_i, !rst_ni) + `ASSERT(ReqAndReadyImplyGrant_A, |req_i && ready_i |-> |gnt_o) // A request and a sink that is ready imply a grant - `ASSERT(ReqImpliesValid_A, |req_i |-> valid_o, clk_i, !rst_ni) + `ASSERT(ReqImpliesValid_A, |req_i |-> valid_o) // Both conditions above combined and reversed - `ASSERT(ReadyAndValidImplyGrant_A, ready_i && valid_o |-> |gnt_o, clk_i, !rst_ni) + `ASSERT(ReadyAndValidImplyGrant_A, ready_i && valid_o |-> |gnt_o) // Both conditions above combined and reversed - `ASSERT(NoReadyValidNoGrant_A, !(ready_i || valid_o) |-> gnt_o == 0, clk_i, !rst_ni) + `ASSERT(NoReadyValidNoGrant_A, !(ready_i || valid_o) |-> gnt_o == 0) // check index / grant correspond - `ASSERT(IndexIsCorrect_A, ready_i && valid_o |-> gnt_o[idx_o] && req_i[idx_o], clk_i, !rst_ni) + `ASSERT(IndexIsCorrect_A, ready_i && valid_o |-> gnt_o[idx_o] && req_i[idx_o]) // data flow - `ASSERT(DataFlow_A, ready_i && valid_o |-> data_o == data_i[idx_o], clk_i, !rst_ni) + `ASSERT(DataFlow_A, ready_i && valid_o |-> data_o == data_i[idx_o]) // KNOWN assertions on outputs, except for data as that may be partially X in simulation // e.g. when used on a BUS - `ASSERT_KNOWN(ValidKnown_A, valid_o, clk_i, !rst_ni) - `ASSERT_KNOWN(GrantKnown_A, gnt_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IdxKnown_A, idx_o, clk_i, !rst_ni) + `ASSERT_KNOWN(ValidKnown_A, valid_o) + `ASSERT_KNOWN(GrantKnown_A, gnt_o) + `ASSERT_KNOWN(IdxKnown_A, idx_o) `ifndef SYNTHESIS // A grant implies a request int unsigned k; // this is a symbolic variable `ASSUME(KStable_M, ##1 $stable(k), clk_i, !rst_ni) `ASSUME(KRange_M, k < N, clk_i, !rst_ni) - `ASSERT(GntImpliesReq_A, gnt_o[k] |-> req_i[k], clk_i, !rst_ni) + `ASSERT(GntImpliesReq_A, gnt_o[k] |-> req_i[k]) // requests must stay asserted until they have been granted `ASSUME(ReqStaysHighUntilGranted_M, (|req_i) && !ready_i |=> - (req_i & $past(req_i)) == $past(req_i), clk_i, !rst_ni) + (req_i & $past(req_i)) == $past(req_i)) // check that the arbitration decision is held if the sink is not ready - `ASSERT(LockArbDecision_A, |req_i && !ready_i |=> idx_o == $past(idx_o), clk_i, !rst_ni) + `ASSERT(LockArbDecision_A, |req_i && !ready_i |=> idx_o == $past(idx_o)) `endif
diff --git a/hw/ip/prim/rtl/prim_arbiter_tree.sv b/hw/ip/prim/rtl/prim_arbiter_tree.sv index 5ec483e..2762a64 100644 --- a/hw/ip/prim/rtl/prim_arbiter_tree.sv +++ b/hw/ip/prim/rtl/prim_arbiter_tree.sv
@@ -179,42 +179,42 @@ //////////////// // we can only grant one requestor at a time - `ASSERT(CheckHotOne_A, $onehot0(gnt_o), clk_i, !rst_ni) + `ASSERT(CheckHotOne_A, $onehot0(gnt_o)) // A grant implies that the sink is ready - `ASSERT(GntImpliesReady_A, |gnt_o |-> ready_i, clk_i, !rst_ni) + `ASSERT(GntImpliesReady_A, |gnt_o |-> ready_i) // A grant implies that the arbiter asserts valid as well - `ASSERT(GntImpliesValid_A, |gnt_o |-> valid_o, clk_i, !rst_ni) + `ASSERT(GntImpliesValid_A, |gnt_o |-> valid_o) // A request and a sink that is ready imply a grant - `ASSERT(ReqAndReadyImplyGrant_A, |req_i && ready_i |-> |gnt_o, clk_i, !rst_ni) + `ASSERT(ReqAndReadyImplyGrant_A, |req_i && ready_i |-> |gnt_o) // A request and a sink that is ready imply a grant - `ASSERT(ReqImpliesValid_A, |req_i |-> valid_o, clk_i, !rst_ni) + `ASSERT(ReqImpliesValid_A, |req_i |-> valid_o) // Both conditions above combined and reversed - `ASSERT(ReadyAndValidImplyGrant_A, ready_i && valid_o |-> |gnt_o, clk_i, !rst_ni) + `ASSERT(ReadyAndValidImplyGrant_A, ready_i && valid_o |-> |gnt_o) // Both conditions above combined and reversed - `ASSERT(NoReadyValidNoGrant_A, !(ready_i || valid_o) |-> gnt_o == 0, clk_i, !rst_ni) + `ASSERT(NoReadyValidNoGrant_A, !(ready_i || valid_o) |-> gnt_o == 0) // check index / grant correspond - `ASSERT(IndexIsCorrect_A, ready_i && valid_o |-> gnt_o[idx_o] && req_i[idx_o], clk_i, !rst_ni) + `ASSERT(IndexIsCorrect_A, ready_i && valid_o |-> gnt_o[idx_o] && req_i[idx_o]) // data flow - `ASSERT(DataFlow_A, ready_i && valid_o |-> data_o == data_i[idx_o], clk_i, !rst_ni) + `ASSERT(DataFlow_A, ready_i && valid_o |-> data_o == data_i[idx_o]) // KNOWN assertions on outputs, except for data as that may be partially X in simulation // e.g. when used on a BUS - `ASSERT_KNOWN(ValidKnown_A, valid_o, clk_i, !rst_ni) - `ASSERT_KNOWN(GrantKnown_A, gnt_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IdxKnown_A, idx_o, clk_i, !rst_ni) + `ASSERT_KNOWN(ValidKnown_A, valid_o) + `ASSERT_KNOWN(GrantKnown_A, gnt_o) + `ASSERT_KNOWN(IdxKnown_A, idx_o) `ifndef SYNTHESIS // A grant implies a request int unsigned k; // this is a symbolic variable `ASSUME(KStable_M, ##1 $stable(k), clk_i, !rst_ni) `ASSUME(KRange_M, k < N, clk_i, !rst_ni) - `ASSERT(GntImpliesReq_A, gnt_o[k] |-> req_i[k], clk_i, !rst_ni) + `ASSERT(GntImpliesReq_A, gnt_o[k] |-> req_i[k]) if (Lock) begin : gen_lock_assertion // requests must stay asserted until they have been granted `ASSUME(ReqStaysHighUntilGranted_M, (|req_i) && !ready_i |=> (req_i & $past(req_i)) == $past(req_i), clk_i, !rst_ni) // check that the arbitration decision is held if the sink is not ready - `ASSERT(LockArbDecision_A, |req_i && !ready_i |=> idx_o == $past(idx_o), clk_i, !rst_ni) + `ASSERT(LockArbDecision_A, |req_i && !ready_i |=> idx_o == $past(idx_o)) end `endif
diff --git a/hw/ip/prim/rtl/prim_assert.sv b/hw/ip/prim/rtl/prim_assert.sv index 588a432..f569292 100644 --- a/hw/ip/prim/rtl/prim_assert.sv +++ b/hw/ip/prim/rtl/prim_assert.sv
@@ -47,6 +47,10 @@ // Simple assertion and cover macros // /////////////////////////////////////// +// Default clk and reset signals used by assertion macros below. +`define ASSERT_DEFAULT_CLK clk_i +`define ASSERT_DEFAULT_RST !rst_ni + // Immediate assertion // Note that immediate assertions are sensitive to simulation glitches. `define ASSERT_I(__name, __prop) \ @@ -75,10 +79,10 @@ // Assert a concurrent property directly. // It can be called as a module (or interface) body item. -`define ASSERT(__name, __prop, __clk, __rst) \ -`ifdef INC_ASSERT \ - __name: assert property (@(posedge __clk) disable iff (__rst !== '0) (__prop)) \ - else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \ +`define ASSERT(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + __name: assert property (@(posedge __clk) disable iff (__rst !== '0) (__prop)) \ + else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \ `endif // Note: Above we use (__rst !== '0) in the disable iff statements instead of // (__rst == '1). This properly disables the assertion in cases when reset is X at @@ -86,23 +90,23 @@ // assertion. // Assert a concurrent property NEVER happens -`define ASSERT_NEVER(__name, __prop, __clk, __rst) \ -`ifdef INC_ASSERT \ - __name: assert property (@(posedge __clk) disable iff (__rst !== '0) not (__prop)) \ - else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \ +`define ASSERT_NEVER(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + __name: assert property (@(posedge __clk) disable iff (__rst !== '0) not (__prop)) \ + else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \ `endif // Assert that signal has a known value (each bit is either '0' or '1') after reset. // It can be called as a module (or interface) body item. -`define ASSERT_KNOWN(__name, __sig, __clk, __rst) \ -`ifdef INC_ASSERT \ - `ASSERT(__name, !$isunknown(__sig), __clk, __rst) \ +`define ASSERT_KNOWN(__name, __sig, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + `ASSERT(__name, !$isunknown(__sig), __clk, __rst) \ `endif // Cover a concurrent property -`define COVER(__name, __prop, __clk, __rst) \ -`ifdef INC_ASSERT \ - __name: cover property (@(posedge __clk) disable iff (__rst !== '0) (__prop)); \ +`define COVER(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + __name: cover property (@(posedge __clk) disable iff (__rst !== '0) (__prop)); \ `endif ////////////////////////////// @@ -110,24 +114,24 @@ ////////////////////////////// // Assert that signal is an active-high pulse with pulse length of 1 clock cycle -`define ASSERT_PULSE(__name, __sig, __clk, __rst) \ -`ifdef INC_ASSERT \ - `ASSERT(__name, $rose(__sig) |=> !(__sig), __clk, __rst) \ +`define ASSERT_PULSE(__name, __sig, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + `ASSERT(__name, $rose(__sig) |=> !(__sig), __clk, __rst) \ `endif // Assert that valid is known after reset and data is known when valid == 1 -`define ASSERT_VALID_DATA(__name, __valid, __dat, __clk, __rst) \ -`ifdef INC_ASSERT \ - `ASSERT_KNOWN(__name``KnownValid, __valid, __clk, __rst) \ - `ASSERT_NEVER(__name``KnownData, (__valid) && $isunknown(__dat), __clk, __rst) \ +`define ASSERT_VALID_DATA(__name, __valid, __dat, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + `ASSERT_KNOWN(__name``KnownValid, __valid, __clk, __rst) \ + `ASSERT_NEVER(__name``KnownData, (__valid) && $isunknown(__dat), __clk, __rst) \ `endif // Same as ASSERT_VALID_DATA, but also assert that ready is known after reset -`define ASSERT_VALID_READY_DATA(__name, __valid, __ready, __dat, __clk, __rst) \ -`ifdef INC_ASSERT \ - `ASSERT_KNOWN(__name``KnownValid, __valid, __clk, __rst) \ - `ASSERT_KNOWN(__name``KnownReady, __ready, __clk, __rst) \ - `ASSERT_NEVER(__name``KnownData, (__valid) && $isunknown(__dat), __clk, __rst) \ +`define ASSERT_VALID_READY_DATA(__name, __valid, __ready, __dat, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + `ASSERT_KNOWN(__name``KnownValid, __valid, __clk, __rst) \ + `ASSERT_KNOWN(__name``KnownReady, __ready, __clk, __rst) \ + `ASSERT_NEVER(__name``KnownData, (__valid) && $isunknown(__dat), __clk, __rst) \ `endif /////////////////////// @@ -135,10 +139,10 @@ /////////////////////// // Assume a concurrent property -`define ASSUME(__name, __prop, __clk, __rst) \ -`ifdef INC_ASSERT \ - __name: assume property (@(posedge __clk) disable iff (__rst !== '0) (__prop)) \ - else begin `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) end \ +`define ASSUME(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + __name: assume property (@(posedge __clk) disable iff (__rst !== '0) (__prop)) \ + else begin `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) end \ `endif // Assume an immediate property @@ -157,9 +161,9 @@ // ASSUME_FPV // Assume a concurrent property during formal verification only. -`define ASSUME_FPV(__name, __prop, __clk, __rst) \ -`ifdef FPV_ON \ - `ASSUME(__name, __prop, __clk, __rst) \ +`define ASSUME_FPV(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef FPV_ON \ + `ASSUME(__name, __prop, __clk, __rst) \ `endif // ASSUME_I_FPV @@ -171,9 +175,9 @@ // COVER_FPV // Cover a concurrent property during formal verification -`define COVER_FPV(__name, __prop, __clk, __rst) \ -`ifdef FPV_ON \ - `COVER(__name, __prop, __clk, __rst) \ +`define COVER_FPV(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef FPV_ON \ + `COVER(__name, __prop, __clk, __rst) \ `endif `endif // PRIM_ASSERT_SV
diff --git a/hw/ip/prim/rtl/prim_diff_decode.sv b/hw/ip/prim/rtl/prim_diff_decode.sv index ab5ac0d..3a1c27a 100644 --- a/hw/ip/prim/rtl/prim_diff_decode.sv +++ b/hw/ip/prim/rtl/prim_diff_decode.sv
@@ -211,29 +211,29 @@ // shared assertions // sigint -> level stays the same during sigint // $isunknown is needed to avoid false assertion in first clock cycle - `ASSERT(SigintLevelCheck_A, ##1 sigint_o |-> $stable(level_o), clk_i, !rst_ni) + `ASSERT(SigintLevelCheck_A, ##1 sigint_o |-> $stable(level_o)) // sigint -> no additional events asserted at output - `ASSERT(SigintEventCheck_A, sigint_o |-> !event_o, clk_i, !rst_ni) - `ASSERT(SigintRiseCheck_A, sigint_o |-> !rise_o, clk_i, !rst_ni) - `ASSERT(SigintFallCheck_A, sigint_o |-> !fall_o, clk_i, !rst_ni) + `ASSERT(SigintEventCheck_A, sigint_o |-> !event_o) + `ASSERT(SigintRiseCheck_A, sigint_o |-> !rise_o) + `ASSERT(SigintFallCheck_A, sigint_o |-> !fall_o) if (AsyncOn) begin : gen_async_assert // assertions for asynchronous case // correctly detect sigint issue (only one transition cycle of permissible due to skew) - `ASSERT(SigintCheck0_A, diff_pi == diff_ni [*2] |-> ##[1:2] sigint_o, clk_i, !rst_ni) + `ASSERT(SigintCheck0_A, diff_pi == diff_ni [*2] |-> ##[1:2] sigint_o) // the synchronizer adds 2 cycles of latency `ASSERT(SigintCheck1_A, ##1 (diff_pi ^ diff_ni) && $stable(diff_pi) && $stable(diff_ni) ##1 $rose(diff_pi) && $stable(diff_ni) ##1 $stable(diff_pi) && $fell(diff_ni) |-> - ##2 rise_o, clk_i, !rst_ni) + ##2 rise_o) `ASSERT(SigintCheck2_A, ##1 (diff_pi ^ diff_ni) && $stable(diff_pi) && $stable(diff_ni) ##1 $fell(diff_pi) && $stable(diff_ni) ##1 $stable(diff_pi) && $rose(diff_ni) |-> - ##2 fall_o, clk_i, !rst_ni) + ##2 fall_o) `ASSERT(SigintCheck3_A, ##1 (diff_pi ^ diff_ni) && $stable(diff_pi) && $stable(diff_ni) ##1 $rose(diff_ni) && $stable(diff_pi) ##1 $stable(diff_ni) && $fell(diff_pi) |-> - ##2 fall_o, clk_i, !rst_ni) + ##2 fall_o) `ASSERT(SigintCheck4_A, ##1 (diff_pi ^ diff_ni) && $stable(diff_pi) && $stable(diff_ni) ##1 $fell(diff_ni) && $stable(diff_pi) ##1 $stable(diff_ni) && $rose(diff_pi) |-> - ##2 rise_o, clk_i, !rst_ni) + ##2 rise_o) // correctly detect edges `ASSERT(RiseCheck_A, ##1 $rose(diff_pi) && (diff_pi ^ diff_ni) |-> ##[2:3] rise_o, clk_i, !rst_ni || sigint_o) @@ -248,13 +248,13 @@ end else begin : gen_sync_assert // assertions for synchronous case // correctly detect sigint issue - `ASSERT(SigintCheck_A, diff_pi == diff_ni |-> sigint_o, clk_i, !rst_ni) + `ASSERT(SigintCheck_A, diff_pi == diff_ni |-> sigint_o) // correctly detect edges - `ASSERT(RiseCheck_A, ##1 $rose(diff_pi) && (diff_pi ^ diff_ni) |-> rise_o, clk_i, !rst_ni) - `ASSERT(FallCheck_A, ##1 $fell(diff_pi) && (diff_pi ^ diff_ni) |-> fall_o, clk_i, !rst_ni) - `ASSERT(EventCheck_A, ##1 $changed(diff_pi) && (diff_pi ^ diff_ni) |-> event_o, clk_i, !rst_ni) + `ASSERT(RiseCheck_A, ##1 $rose(diff_pi) && (diff_pi ^ diff_ni) |-> rise_o) + `ASSERT(FallCheck_A, ##1 $fell(diff_pi) && (diff_pi ^ diff_ni) |-> fall_o) + `ASSERT(EventCheck_A, ##1 $changed(diff_pi) && (diff_pi ^ diff_ni) |-> event_o) // correctly detect level - `ASSERT(LevelCheck_A, (diff_pi ^ diff_ni) |-> diff_pi == level_o, clk_i, !rst_ni) + `ASSERT(LevelCheck_A, (diff_pi ^ diff_ni) |-> diff_pi == level_o) end endmodule : prim_diff_decode
diff --git a/hw/ip/prim/rtl/prim_esc_receiver.sv b/hw/ip/prim/rtl/prim_esc_receiver.sv index 5d8c0b8..52e86d1 100644 --- a/hw/ip/prim/rtl/prim_esc_receiver.sv +++ b/hw/ip/prim/rtl/prim_esc_receiver.sv
@@ -154,15 +154,15 @@ //////////////// // check whether all outputs have a good known state after reset - `ASSERT_KNOWN(EscEnKnownO_A, esc_en_o, clk_i, !rst_ni) - `ASSERT_KNOWN(RespPKnownO_A, esc_rx_o, clk_i, !rst_ni) + `ASSERT_KNOWN(EscEnKnownO_A, esc_en_o) + `ASSERT_KNOWN(RespPKnownO_A, esc_rx_o) `ASSERT(SigIntCheck0_A, esc_tx_i.esc_p == esc_tx_i.esc_n |=> esc_rx_o.resp_p == esc_rx_o.resp_n, clk_i, !rst_ni) - `ASSERT(SigIntCheck1_A, esc_tx_i.esc_p == esc_tx_i.esc_n |=> state_q == SigInt, clk_i, !rst_ni) + `ASSERT(SigIntCheck1_A, esc_tx_i.esc_p == esc_tx_i.esc_n |=> state_q == SigInt) // correct diff encoding `ASSERT(DiffEncCheck_A, esc_tx_i.esc_p ^ esc_tx_i.esc_n |=> - esc_rx_o.resp_p ^ esc_rx_o.resp_n, clk_i, !rst_ni) + esc_rx_o.resp_p ^ esc_rx_o.resp_n) // disable in case of ping integrity issue `ASSERT(PingRespCheck_A, $rose(esc_tx_i.esc_p) |=> $fell(esc_tx_i.esc_p) |-> $rose(esc_rx_o.resp_p) |=> $fell(esc_rx_o.resp_p), @@ -170,9 +170,9 @@ // escalation response needs to continuously toggle `ASSERT(EscRespCheck_A, esc_tx_i.esc_p && $past(esc_tx_i.esc_p) && (esc_tx_i.esc_p ^ esc_tx_i.esc_n) && $past(esc_tx_i.esc_p ^ esc_tx_i.esc_n) - |=> esc_rx_o.resp_p != $past(esc_rx_o.resp_p), clk_i, !rst_ni) + |=> esc_rx_o.resp_p != $past(esc_rx_o.resp_p)) // detect escalation pulse `ASSERT(EscEnCheck_A, esc_tx_i.esc_p && (esc_tx_i.esc_p ^ esc_tx_i.esc_n) && state_q != SigInt - |=> esc_tx_i.esc_p && (esc_tx_i.esc_p ^ esc_tx_i.esc_n) |-> esc_en_o, clk_i, !rst_ni ) + |=> esc_tx_i.esc_p && (esc_tx_i.esc_p ^ esc_tx_i.esc_n) |-> esc_en_o) endmodule : prim_esc_receiver
diff --git a/hw/ip/prim/rtl/prim_esc_sender.sv b/hw/ip/prim/rtl/prim_esc_sender.sv index 0784329..16107e6 100644 --- a/hw/ip/prim/rtl/prim_esc_sender.sv +++ b/hw/ip/prim/rtl/prim_esc_sender.sv
@@ -210,14 +210,14 @@ //////////////// // check whether all outputs have a good known state after reset - `ASSERT_KNOWN(PingOkKnownO_A, ping_ok_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntegFailKnownO_A, integ_fail_o, clk_i, !rst_ni) - `ASSERT_KNOWN(EscPKnownO_A, esc_tx_o, clk_i, !rst_ni) + `ASSERT_KNOWN(PingOkKnownO_A, ping_ok_o) + `ASSERT_KNOWN(IntegFailKnownO_A, integ_fail_o) + `ASSERT_KNOWN(EscPKnownO_A, esc_tx_o) // diff encoding of output - `ASSERT(DiffEncCheck_A, esc_tx_o.esc_p ^ esc_tx_o.esc_n, clk_i, !rst_ni) + `ASSERT(DiffEncCheck_A, esc_tx_o.esc_p ^ esc_tx_o.esc_n) // signal integrity check propagation - `ASSERT(SigIntCheck0_A, esc_rx_i.resp_p == esc_rx_i.resp_n |-> integ_fail_o, clk_i, !rst_ni) + `ASSERT(SigIntCheck0_A, esc_rx_i.resp_p == esc_rx_i.resp_n |-> integ_fail_o) // this happens in case we did not get a correct escalation response `ASSERT(SigIntCheck1_A, ##1 $rose(esc_en_i) && state_q inside {Idle, CheckPingResp1, CheckPingResp3} ##1 !esc_rx_i.resp_p |-> @@ -228,9 +228,9 @@ integ_fail_o, clk_i, !rst_ni || (esc_rx_i.resp_p == esc_rx_i.resp_n) || (state_q == Idle && resp)) // unexpected response - `ASSERT(SigIntCheck3_A, state_q == Idle && resp |-> integ_fail_o, clk_i, !rst_ni) + `ASSERT(SigIntCheck3_A, state_q == Idle && resp |-> integ_fail_o) // check that escalation signal is at least 2 cycles high - `ASSERT(EscCheck_A, esc_en_i |-> esc_tx_o.esc_p [*2] , clk_i, !rst_ni) + `ASSERT(EscCheck_A, esc_en_i |-> esc_tx_o.esc_p [*2] ) // escalation / ping collision `ASSERT(EscPingCheck_A, esc_en_i && ping_en_i |-> ping_ok_o, clk_i, !rst_ni || integ_fail_o) // check that ping request results in only a single cycle pulse
diff --git a/hw/ip/prim/rtl/prim_fifo_sync.sv b/hw/ip/prim/rtl/prim_fifo_sync.sv index 5d10b97..e2199db 100644 --- a/hw/ip/prim/rtl/prim_fifo_sync.sv +++ b/hw/ip/prim/rtl/prim_fifo_sync.sv
@@ -139,7 +139,7 @@ assign empty = fifo_empty; end - `ASSERT(depthShallNotExceedParamDepth, !empty |-> depth <= DepthW'(Depth), clk_i, !rst_ni) + `ASSERT(depthShallNotExceedParamDepth, !empty |-> depth <= DepthW'(Depth)) end // block: gen_normal_fifo @@ -147,9 +147,9 @@ // Known Assertions // ////////////////////// - `ASSERT(DataKnown_A, rvalid |-> !$isunknown(rdata), clk_i, !rst_ni) - `ASSERT_KNOWN(DepthKnown_A, depth, clk_i, !rst_ni) - `ASSERT_KNOWN(RvalidKnown_A, rvalid, clk_i, !rst_ni) - `ASSERT_KNOWN(WreadyKnown_A, wready, clk_i, !rst_ni) + `ASSERT(DataKnown_A, rvalid |-> !$isunknown(rdata)) + `ASSERT_KNOWN(DepthKnown_A, depth) + `ASSERT_KNOWN(RvalidKnown_A, rvalid) + `ASSERT_KNOWN(WreadyKnown_A, wready) endmodule
diff --git a/hw/ip/prim/rtl/prim_lfsr.sv b/hw/ip/prim/rtl/prim_lfsr.sv index 05592b2..3c162be 100644 --- a/hw/ip/prim/rtl/prim_lfsr.sv +++ b/hw/ip/prim/rtl/prim_lfsr.sv
@@ -378,7 +378,7 @@ // shared assertions // /////////////////////// - `ASSERT_KNOWN(DataKnownO_A, state_o, clk_i, !rst_ni) + `ASSERT_KNOWN(DataKnownO_A, state_o) // the code below is not meant to be synthesized, // but it is intended to be used in simulation and FPV @@ -417,29 +417,27 @@ // check whether next state is computed correctly `ASSERT(NextStateCheck_A, lfsr_en_i && !seed_en_i |=> lfsr_q == - compute_next_state(coeffs, $past(entropy_i,1), $past(lfsr_q,1)), - clk_i, !rst_ni ) + compute_next_state(coeffs, $past(entropy_i,1), $past(lfsr_q,1))) `endif `ASSERT_INIT(InputWidth_A, LfsrDw >= EntropyDw) `ASSERT_INIT(OutputWidth_A, LfsrDw >= StateOutDw) // MSB must be one in any case - `ASSERT(CoeffCheck_A, coeffs[LfsrDw-1], clk_i, !rst_ni) + `ASSERT(CoeffCheck_A, coeffs[LfsrDw-1]) // output check - `ASSERT_KNOWN(OutputKnown_A, state_o, clk_i, !rst_ni) - `ASSERT(OutputCheck_A, state_o == StateOutDw'(lfsr_q), clk_i, !rst_ni) + `ASSERT_KNOWN(OutputKnown_A, state_o) + `ASSERT(OutputCheck_A, state_o == StateOutDw'(lfsr_q)) // if no external input changes the lfsr state, a lockup must not occur (by design) //`ASSERT(NoLockups_A, (!entropy_i) && (!seed_en_i) |=> !lockup, clk_i, !rst_ni) - `ASSERT(NoLockups_A, lfsr_en_i && !entropy_i && !seed_en_i |=> !lockup, clk_i, !rst_ni) + `ASSERT(NoLockups_A, lfsr_en_i && !entropy_i && !seed_en_i |=> !lockup) // this can be disabled if unused in order to not distort coverage if (ExtSeedSVA) begin : gen_ext_seed_sva // check that external seed is correctly loaded into the state - `ASSERT(ExtDefaultSeedInputCheck_A, seed_en_i |=> lfsr_q == $past(seed_i), - clk_i, !rst_ni) + `ASSERT(ExtDefaultSeedInputCheck_A, seed_en_i |=> lfsr_q == $past(seed_i)) end // if the external seed mechanism is not used, @@ -447,8 +445,7 @@ // in order to not distort coverage, this SVA can be disabled in such cases if (LockupSVA) begin : gen_lockup_mechanism_sva // check that a stuck LFSR is correctly reseeded - `ASSERT(LfsrLockupCheck_A, lfsr_en_i && lockup && !seed_en_i |=> !lockup, - clk_i, !rst_ni) + `ASSERT(LfsrLockupCheck_A, lfsr_en_i && lockup && !seed_en_i |=> !lockup) end if (MaxLenSVA) begin : gen_max_len_sva
diff --git a/hw/ip/prim/rtl/prim_packer.sv b/hw/ip/prim/rtl/prim_packer.sv index 4d78994..b7ad437 100644 --- a/hw/ip/prim/rtl/prim_packer.sv +++ b/hw/ip/prim/rtl/prim_packer.sv
@@ -200,8 +200,7 @@ // e.g: 0011100 --> OK // 0100011 --> Not OK `ASSUME(ContiguousOnesMask_M, - valid_i |-> $countones(mask_i ^ {mask_i[InW-2:0],1'b0}) <= 2, - clk_i, !rst_ni) + valid_i |-> $countones(mask_i ^ {mask_i[InW-2:0],1'b0}) <= 2) // Assume data pattern to reduce FPV test time //`ASSUME_FPV(FpvDataWithin_M, @@ -209,41 +208,34 @@ // clk_i, !rst_ni) // Flush and Write Enable cannot be asserted same time - `ASSUME(ExFlushValid_M, flush_i |-> !valid_i, clk_i, !rst_ni) + `ASSUME(ExFlushValid_M, flush_i |-> !valid_i) // While in flush state, new request shouldn't come `ASSUME(ValidIDeassertedOnFlush_M, - flush_st == FlushWait |-> $stable(valid_i), - clk_i, !rst_ni) + flush_st == FlushWait |-> $stable(valid_i)) // If not acked, input port keeps asserting valid and data `ASSUME(DataIStable_M, ##1 valid_i && $past(valid_i) && !$past(ready_o) - |-> $stable(data_i) && $stable(mask_i), - clk_i, !rst_ni) + |-> $stable(data_i) && $stable(mask_i)) `ASSUME(ValidIPairedWithReadyO_M, - valid_i && !ready_o |=> valid_i, - clk_i, !rst_ni) + valid_i && !ready_o |=> valid_i) `ASSERT(FlushFollowedByDone_A, - ##1 $rose(flush_i) && !flush_done_o |-> !flush_done_o [*0:$] ##1 flush_done_o, - clk_i, !rst_ni) + ##1 $rose(flush_i) && !flush_done_o |-> !flush_done_o [*0:$] ##1 flush_done_o) // If not acked, valid_o should keep asserting `ASSERT(ValidOPairedWidthReadyI_A, - valid_o && !ready_i |=> valid_o, - clk_i, !rst_ni) + valid_o && !ready_i |=> valid_o) // If input mask + stored data is greater than output width, valid should be asserted `ASSERT(ValidOAssertedForInputGTEOutW_A, - valid_i && (($countones(mask_i) + $countones(stored_mask)) >= OutW) |-> valid_o, - clk_i, !rst_ni) + valid_i && (($countones(mask_i) + $countones(stored_mask)) >= OutW) |-> valid_o) // If output port doesn't accept the data, the data should be stable `ASSERT(DataOStableWhenPending_A, ##1 valid_o && $past(valid_o) - && !$past(ready_i) |-> $stable(data_o), - clk_i, !rst_ni) + && !$past(ready_i) |-> $stable(data_o)) // If input data & stored data are greater than OutW, remained should be stored // TODO: Find out how the FPV time can be reduced. @@ -257,7 +249,6 @@ ack_in && (($countones(mask_i) + $countones(stored_mask)) > OutW) |=> ($past(mask_i) >> ($past(lod_idx)+OutW-$countones($past(stored_mask)))) - == stored_mask, - clk_i, !rst_ni) + == stored_mask) endmodule
diff --git a/hw/ip/rv_dm/rtl/tlul_adapter_host.sv b/hw/ip/rv_dm/rtl/tlul_adapter_host.sv index 2622c36..3961f90 100644 --- a/hw/ip/rv_dm/rtl/tlul_adapter_host.sv +++ b/hw/ip/rv_dm/rtl/tlul_adapter_host.sv
@@ -53,6 +53,6 @@ assign rdata_o = tl_i.d_data; // this assertion fails when DBG adapter cannot handle error response - `ASSERT(handleErrorResponse, tl_i.d_valid |-> (tl_i.d_error == 1'b0), clk_i, !rst_ni) + `ASSERT(handleErrorResponse, tl_i.d_valid |-> (tl_i.d_error == 1'b0)) endmodule
diff --git a/hw/ip/rv_plic/data/rv_plic.sv.tpl b/hw/ip/rv_plic/data/rv_plic.sv.tpl index b6c56a3..a4fe14d 100644 --- a/hw/ip/rv_plic/data/rv_plic.sv.tpl +++ b/hw/ip/rv_plic/data/rv_plic.sv.tpl
@@ -78,12 +78,12 @@ end end - //`ASSERT_PULSE(claimPulse, claim_re[i], clk_i, !rst_ni) - //`ASSERT_PULSE(completePulse, complete_we[i], clk_i, !rst_ni) + //`ASSERT_PULSE(claimPulse, claim_re[i]) + //`ASSERT_PULSE(completePulse, complete_we[i]) - `ASSERT(onehot0Claim, $onehot0(claim_re), clk_i, !rst_ni) + `ASSERT(onehot0Claim, $onehot0(claim_re)) - `ASSERT(onehot0Complete, $onehot0(complete_we), clk_i, !rst_ni) + `ASSERT(onehot0Complete, $onehot0(complete_we)) ////////////// // Priority // @@ -201,12 +201,12 @@ ); // Assertions - `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid, clk_i, !rst_ni) - `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready, clk_i, !rst_ni) - `ASSERT_KNOWN(IrqKnownO_A, irq_o, clk_i, !rst_ni) - `ASSERT_KNOWN(MsipKnownO_A, msip_o, clk_i, !rst_ni) + `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid) + `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready) + `ASSERT_KNOWN(IrqKnownO_A, irq_o) + `ASSERT_KNOWN(MsipKnownO_A, msip_o) for (genvar k = 0; k < NumTarget; k++) begin : gen_irq_id_known - `ASSERT_KNOWN(IrqIdKnownO_A, irq_id_o[k], clk_i, !rst_ni) + `ASSERT_KNOWN(IrqIdKnownO_A, irq_id_o[k]) end endmodule
diff --git a/hw/ip/rv_plic/fpv/vip/rv_plic_assert_fpv.sv b/hw/ip/rv_plic/fpv/vip/rv_plic_assert_fpv.sv index 774780d..afbd8cd 100644 --- a/hw/ip/rv_plic/fpv/vip/rv_plic_assert_fpv.sv +++ b/hw/ip/rv_plic/fpv/vip/rv_plic_assert_fpv.sv
@@ -74,34 +74,33 @@ // when IP is set, previous cycle should follow edge or level triggered criteria `ASSERT(LevelTriggeredIp_A, $rose(ip[src_sel]) |-> - $past(le[src_sel]) || $past(intr_src_i[src_sel]), clk_i, !rst_ni) + $past(le[src_sel]) || $past(intr_src_i[src_sel])) `ASSERT(EdgeTriggeredIp_A, $rose(ip[src_sel]) |-> - !$past(le[src_sel]) || $rose($past(intr_src_i[src_sel])), clk_i, !rst_ni) + !$past(le[src_sel]) || $rose($past(intr_src_i[src_sel]))) // when interrupt is trigger, and nothing claimed yet, then next cycle should assert IP. `ASSERT(LevelTriggeredIpWithClaim_A, !le[src_sel] && intr_src_i[src_sel] && !claimed |=> - ip[src_sel], clk_i, !rst_ni) + ip[src_sel]) `ASSERT(EdgeTriggeredIpWithClaim_A, le[src_sel] && $rose(intr_src_i[src_sel]) && !claimed |=> - ip[src_sel], clk_i, !rst_ni) + ip[src_sel]) // ip stays stable until claimed, reset to 0 after claimed, and stays 0 until complete - `ASSERT(IpStableAfterTriggered_A, ip[src_sel] && !claimed |=> ip[src_sel], clk_i, !rst_ni) - `ASSERT(IpClearAfterClaim_A, ip[src_sel] && claim[src_sel] |=> !ip[src_sel], clk_i, !rst_ni) - `ASSERT(IpStableAfterClaimed_A, claimed |=> !ip[src_sel], clk_i, !rst_ni) + `ASSERT(IpStableAfterTriggered_A, ip[src_sel] && !claimed |=> ip[src_sel]) + `ASSERT(IpClearAfterClaim_A, ip[src_sel] && claim[src_sel] |=> !ip[src_sel]) + `ASSERT(IpStableAfterClaimed_A, claimed |=> !ip[src_sel]) // when ip is set and priority is the largest and above threshold, and interrupt enable is set, // assertion irq_o at next cycle `ASSERT(TriggerIrqForwardCheck_A, ip[src_sel] && prio[src_sel] > threshold[tgt_sel] && - max_priority && ie[tgt_sel][src_sel] |=> irq_o[tgt_sel], clk_i, !rst_ni) + max_priority && ie[tgt_sel][src_sel] |=> irq_o[tgt_sel]) `ASSERT(TriggerIrqBackwardCheck_A, $rose(irq_o[tgt_sel]) |-> - $past(irq) && (irq_id_o[tgt_sel] - 1) == $past(i_high_prio), clk_i, !rst_ni) + $past(irq) && (irq_id_o[tgt_sel] - 1) == $past(i_high_prio)) // when irq ID changed, but not to ID=0, irq_o should be high, or irq represents the largest prio // but smaller than the threshold `ASSERT(IdChangeWithIrq_A, !$stable(irq_id_o[tgt_sel]) && irq_id_o[tgt_sel] != 0 |-> - irq_o[tgt_sel] || ((irq_id_o[tgt_sel] - 1) == $past(i_high_prio) && !$past(irq)), - clk_i, !rst_ni) + irq_o[tgt_sel] || ((irq_id_o[tgt_sel] - 1) == $past(i_high_prio) && !$past(irq))) endmodule : rv_plic_assert_fpv
diff --git a/hw/ip/rv_plic/fpv/vip/rv_plic_csr_assert_fpv.sv b/hw/ip/rv_plic/fpv/vip/rv_plic_csr_assert_fpv.sv index e01bd6d..8c73e7b 100644 --- a/hw/ip/rv_plic/fpv/vip/rv_plic_csr_assert_fpv.sv +++ b/hw/ip/rv_plic/fpv/vip/rv_plic_csr_assert_fpv.sv
@@ -83,7 +83,7 @@ end // read/write assertions for register: ip - `ASSERT(ip_rd_A, rd_P(31, 9'h0, ip_d_fpv[31:0]), clk_i, !rst_ni) + `ASSERT(ip_rd_A, rd_P(31, 9'h0, ip_d_fpv[31:0])) // define local fpv variable for the multi_reg logic [31:0] le_q_fpv; @@ -92,136 +92,136 @@ end // read/write assertions for register: le - `ASSERT(le_wr_A, wr_P(31, 9'h4, le_q_fpv[31:0], 0), clk_i, !rst_ni) - `ASSERT(le_rd_A, rd_P(31, 9'h4, le_q_fpv[31:0]), clk_i, !rst_ni) + `ASSERT(le_wr_A, wr_P(31, 9'h4, le_q_fpv[31:0], 0)) + `ASSERT(le_rd_A, rd_P(31, 9'h4, le_q_fpv[31:0])) // read/write assertions for register: prio0 - `ASSERT(prio0_wr_A, wr_P(2, 9'h8, i_rv_plic.reg2hw.prio0.q, 0), clk_i, !rst_ni) - `ASSERT(prio0_rd_A, rd_P(2, 9'h8, i_rv_plic.reg2hw.prio0.q), clk_i, !rst_ni) + `ASSERT(prio0_wr_A, wr_P(2, 9'h8, i_rv_plic.reg2hw.prio0.q, 0)) + `ASSERT(prio0_rd_A, rd_P(2, 9'h8, i_rv_plic.reg2hw.prio0.q)) // read/write assertions for register: prio1 - `ASSERT(prio1_wr_A, wr_P(2, 9'hc, i_rv_plic.reg2hw.prio1.q, 0), clk_i, !rst_ni) - `ASSERT(prio1_rd_A, rd_P(2, 9'hc, i_rv_plic.reg2hw.prio1.q), clk_i, !rst_ni) + `ASSERT(prio1_wr_A, wr_P(2, 9'hc, i_rv_plic.reg2hw.prio1.q, 0)) + `ASSERT(prio1_rd_A, rd_P(2, 9'hc, i_rv_plic.reg2hw.prio1.q)) // read/write assertions for register: prio2 - `ASSERT(prio2_wr_A, wr_P(2, 9'h10, i_rv_plic.reg2hw.prio2.q, 0), clk_i, !rst_ni) - `ASSERT(prio2_rd_A, rd_P(2, 9'h10, i_rv_plic.reg2hw.prio2.q), clk_i, !rst_ni) + `ASSERT(prio2_wr_A, wr_P(2, 9'h10, i_rv_plic.reg2hw.prio2.q, 0)) + `ASSERT(prio2_rd_A, rd_P(2, 9'h10, i_rv_plic.reg2hw.prio2.q)) // read/write assertions for register: prio3 - `ASSERT(prio3_wr_A, wr_P(2, 9'h14, i_rv_plic.reg2hw.prio3.q, 0), clk_i, !rst_ni) - `ASSERT(prio3_rd_A, rd_P(2, 9'h14, i_rv_plic.reg2hw.prio3.q), clk_i, !rst_ni) + `ASSERT(prio3_wr_A, wr_P(2, 9'h14, i_rv_plic.reg2hw.prio3.q, 0)) + `ASSERT(prio3_rd_A, rd_P(2, 9'h14, i_rv_plic.reg2hw.prio3.q)) // read/write assertions for register: prio4 - `ASSERT(prio4_wr_A, wr_P(2, 9'h18, i_rv_plic.reg2hw.prio4.q, 0), clk_i, !rst_ni) - `ASSERT(prio4_rd_A, rd_P(2, 9'h18, i_rv_plic.reg2hw.prio4.q), clk_i, !rst_ni) + `ASSERT(prio4_wr_A, wr_P(2, 9'h18, i_rv_plic.reg2hw.prio4.q, 0)) + `ASSERT(prio4_rd_A, rd_P(2, 9'h18, i_rv_plic.reg2hw.prio4.q)) // read/write assertions for register: prio5 - `ASSERT(prio5_wr_A, wr_P(2, 9'h1c, i_rv_plic.reg2hw.prio5.q, 0), clk_i, !rst_ni) - `ASSERT(prio5_rd_A, rd_P(2, 9'h1c, i_rv_plic.reg2hw.prio5.q), clk_i, !rst_ni) + `ASSERT(prio5_wr_A, wr_P(2, 9'h1c, i_rv_plic.reg2hw.prio5.q, 0)) + `ASSERT(prio5_rd_A, rd_P(2, 9'h1c, i_rv_plic.reg2hw.prio5.q)) // read/write assertions for register: prio6 - `ASSERT(prio6_wr_A, wr_P(2, 9'h20, i_rv_plic.reg2hw.prio6.q, 0), clk_i, !rst_ni) - `ASSERT(prio6_rd_A, rd_P(2, 9'h20, i_rv_plic.reg2hw.prio6.q), clk_i, !rst_ni) + `ASSERT(prio6_wr_A, wr_P(2, 9'h20, i_rv_plic.reg2hw.prio6.q, 0)) + `ASSERT(prio6_rd_A, rd_P(2, 9'h20, i_rv_plic.reg2hw.prio6.q)) // read/write assertions for register: prio7 - `ASSERT(prio7_wr_A, wr_P(2, 9'h24, i_rv_plic.reg2hw.prio7.q, 0), clk_i, !rst_ni) - `ASSERT(prio7_rd_A, rd_P(2, 9'h24, i_rv_plic.reg2hw.prio7.q), clk_i, !rst_ni) + `ASSERT(prio7_wr_A, wr_P(2, 9'h24, i_rv_plic.reg2hw.prio7.q, 0)) + `ASSERT(prio7_rd_A, rd_P(2, 9'h24, i_rv_plic.reg2hw.prio7.q)) // read/write assertions for register: prio8 - `ASSERT(prio8_wr_A, wr_P(2, 9'h28, i_rv_plic.reg2hw.prio8.q, 0), clk_i, !rst_ni) - `ASSERT(prio8_rd_A, rd_P(2, 9'h28, i_rv_plic.reg2hw.prio8.q), clk_i, !rst_ni) + `ASSERT(prio8_wr_A, wr_P(2, 9'h28, i_rv_plic.reg2hw.prio8.q, 0)) + `ASSERT(prio8_rd_A, rd_P(2, 9'h28, i_rv_plic.reg2hw.prio8.q)) // read/write assertions for register: prio9 - `ASSERT(prio9_wr_A, wr_P(2, 9'h2c, i_rv_plic.reg2hw.prio9.q, 0), clk_i, !rst_ni) - `ASSERT(prio9_rd_A, rd_P(2, 9'h2c, i_rv_plic.reg2hw.prio9.q), clk_i, !rst_ni) + `ASSERT(prio9_wr_A, wr_P(2, 9'h2c, i_rv_plic.reg2hw.prio9.q, 0)) + `ASSERT(prio9_rd_A, rd_P(2, 9'h2c, i_rv_plic.reg2hw.prio9.q)) // read/write assertions for register: prio10 - `ASSERT(prio10_wr_A, wr_P(2, 9'h30, i_rv_plic.reg2hw.prio10.q, 0), clk_i, !rst_ni) - `ASSERT(prio10_rd_A, rd_P(2, 9'h30, i_rv_plic.reg2hw.prio10.q), clk_i, !rst_ni) + `ASSERT(prio10_wr_A, wr_P(2, 9'h30, i_rv_plic.reg2hw.prio10.q, 0)) + `ASSERT(prio10_rd_A, rd_P(2, 9'h30, i_rv_plic.reg2hw.prio10.q)) // read/write assertions for register: prio11 - `ASSERT(prio11_wr_A, wr_P(2, 9'h34, i_rv_plic.reg2hw.prio11.q, 0), clk_i, !rst_ni) - `ASSERT(prio11_rd_A, rd_P(2, 9'h34, i_rv_plic.reg2hw.prio11.q), clk_i, !rst_ni) + `ASSERT(prio11_wr_A, wr_P(2, 9'h34, i_rv_plic.reg2hw.prio11.q, 0)) + `ASSERT(prio11_rd_A, rd_P(2, 9'h34, i_rv_plic.reg2hw.prio11.q)) // read/write assertions for register: prio12 - `ASSERT(prio12_wr_A, wr_P(2, 9'h38, i_rv_plic.reg2hw.prio12.q, 0), clk_i, !rst_ni) - `ASSERT(prio12_rd_A, rd_P(2, 9'h38, i_rv_plic.reg2hw.prio12.q), clk_i, !rst_ni) + `ASSERT(prio12_wr_A, wr_P(2, 9'h38, i_rv_plic.reg2hw.prio12.q, 0)) + `ASSERT(prio12_rd_A, rd_P(2, 9'h38, i_rv_plic.reg2hw.prio12.q)) // read/write assertions for register: prio13 - `ASSERT(prio13_wr_A, wr_P(2, 9'h3c, i_rv_plic.reg2hw.prio13.q, 0), clk_i, !rst_ni) - `ASSERT(prio13_rd_A, rd_P(2, 9'h3c, i_rv_plic.reg2hw.prio13.q), clk_i, !rst_ni) + `ASSERT(prio13_wr_A, wr_P(2, 9'h3c, i_rv_plic.reg2hw.prio13.q, 0)) + `ASSERT(prio13_rd_A, rd_P(2, 9'h3c, i_rv_plic.reg2hw.prio13.q)) // read/write assertions for register: prio14 - `ASSERT(prio14_wr_A, wr_P(2, 9'h40, i_rv_plic.reg2hw.prio14.q, 0), clk_i, !rst_ni) - `ASSERT(prio14_rd_A, rd_P(2, 9'h40, i_rv_plic.reg2hw.prio14.q), clk_i, !rst_ni) + `ASSERT(prio14_wr_A, wr_P(2, 9'h40, i_rv_plic.reg2hw.prio14.q, 0)) + `ASSERT(prio14_rd_A, rd_P(2, 9'h40, i_rv_plic.reg2hw.prio14.q)) // read/write assertions for register: prio15 - `ASSERT(prio15_wr_A, wr_P(2, 9'h44, i_rv_plic.reg2hw.prio15.q, 0), clk_i, !rst_ni) - `ASSERT(prio15_rd_A, rd_P(2, 9'h44, i_rv_plic.reg2hw.prio15.q), clk_i, !rst_ni) + `ASSERT(prio15_wr_A, wr_P(2, 9'h44, i_rv_plic.reg2hw.prio15.q, 0)) + `ASSERT(prio15_rd_A, rd_P(2, 9'h44, i_rv_plic.reg2hw.prio15.q)) // read/write assertions for register: prio16 - `ASSERT(prio16_wr_A, wr_P(2, 9'h48, i_rv_plic.reg2hw.prio16.q, 0), clk_i, !rst_ni) - `ASSERT(prio16_rd_A, rd_P(2, 9'h48, i_rv_plic.reg2hw.prio16.q), clk_i, !rst_ni) + `ASSERT(prio16_wr_A, wr_P(2, 9'h48, i_rv_plic.reg2hw.prio16.q, 0)) + `ASSERT(prio16_rd_A, rd_P(2, 9'h48, i_rv_plic.reg2hw.prio16.q)) // read/write assertions for register: prio17 - `ASSERT(prio17_wr_A, wr_P(2, 9'h4c, i_rv_plic.reg2hw.prio17.q, 0), clk_i, !rst_ni) - `ASSERT(prio17_rd_A, rd_P(2, 9'h4c, i_rv_plic.reg2hw.prio17.q), clk_i, !rst_ni) + `ASSERT(prio17_wr_A, wr_P(2, 9'h4c, i_rv_plic.reg2hw.prio17.q, 0)) + `ASSERT(prio17_rd_A, rd_P(2, 9'h4c, i_rv_plic.reg2hw.prio17.q)) // read/write assertions for register: prio18 - `ASSERT(prio18_wr_A, wr_P(2, 9'h50, i_rv_plic.reg2hw.prio18.q, 0), clk_i, !rst_ni) - `ASSERT(prio18_rd_A, rd_P(2, 9'h50, i_rv_plic.reg2hw.prio18.q), clk_i, !rst_ni) + `ASSERT(prio18_wr_A, wr_P(2, 9'h50, i_rv_plic.reg2hw.prio18.q, 0)) + `ASSERT(prio18_rd_A, rd_P(2, 9'h50, i_rv_plic.reg2hw.prio18.q)) // read/write assertions for register: prio19 - `ASSERT(prio19_wr_A, wr_P(2, 9'h54, i_rv_plic.reg2hw.prio19.q, 0), clk_i, !rst_ni) - `ASSERT(prio19_rd_A, rd_P(2, 9'h54, i_rv_plic.reg2hw.prio19.q), clk_i, !rst_ni) + `ASSERT(prio19_wr_A, wr_P(2, 9'h54, i_rv_plic.reg2hw.prio19.q, 0)) + `ASSERT(prio19_rd_A, rd_P(2, 9'h54, i_rv_plic.reg2hw.prio19.q)) // read/write assertions for register: prio20 - `ASSERT(prio20_wr_A, wr_P(2, 9'h58, i_rv_plic.reg2hw.prio20.q, 0), clk_i, !rst_ni) - `ASSERT(prio20_rd_A, rd_P(2, 9'h58, i_rv_plic.reg2hw.prio20.q), clk_i, !rst_ni) + `ASSERT(prio20_wr_A, wr_P(2, 9'h58, i_rv_plic.reg2hw.prio20.q, 0)) + `ASSERT(prio20_rd_A, rd_P(2, 9'h58, i_rv_plic.reg2hw.prio20.q)) // read/write assertions for register: prio21 - `ASSERT(prio21_wr_A, wr_P(2, 9'h5c, i_rv_plic.reg2hw.prio21.q, 0), clk_i, !rst_ni) - `ASSERT(prio21_rd_A, rd_P(2, 9'h5c, i_rv_plic.reg2hw.prio21.q), clk_i, !rst_ni) + `ASSERT(prio21_wr_A, wr_P(2, 9'h5c, i_rv_plic.reg2hw.prio21.q, 0)) + `ASSERT(prio21_rd_A, rd_P(2, 9'h5c, i_rv_plic.reg2hw.prio21.q)) // read/write assertions for register: prio22 - `ASSERT(prio22_wr_A, wr_P(2, 9'h60, i_rv_plic.reg2hw.prio22.q, 0), clk_i, !rst_ni) - `ASSERT(prio22_rd_A, rd_P(2, 9'h60, i_rv_plic.reg2hw.prio22.q), clk_i, !rst_ni) + `ASSERT(prio22_wr_A, wr_P(2, 9'h60, i_rv_plic.reg2hw.prio22.q, 0)) + `ASSERT(prio22_rd_A, rd_P(2, 9'h60, i_rv_plic.reg2hw.prio22.q)) // read/write assertions for register: prio23 - `ASSERT(prio23_wr_A, wr_P(2, 9'h64, i_rv_plic.reg2hw.prio23.q, 0), clk_i, !rst_ni) - `ASSERT(prio23_rd_A, rd_P(2, 9'h64, i_rv_plic.reg2hw.prio23.q), clk_i, !rst_ni) + `ASSERT(prio23_wr_A, wr_P(2, 9'h64, i_rv_plic.reg2hw.prio23.q, 0)) + `ASSERT(prio23_rd_A, rd_P(2, 9'h64, i_rv_plic.reg2hw.prio23.q)) // read/write assertions for register: prio24 - `ASSERT(prio24_wr_A, wr_P(2, 9'h68, i_rv_plic.reg2hw.prio24.q, 0), clk_i, !rst_ni) - `ASSERT(prio24_rd_A, rd_P(2, 9'h68, i_rv_plic.reg2hw.prio24.q), clk_i, !rst_ni) + `ASSERT(prio24_wr_A, wr_P(2, 9'h68, i_rv_plic.reg2hw.prio24.q, 0)) + `ASSERT(prio24_rd_A, rd_P(2, 9'h68, i_rv_plic.reg2hw.prio24.q)) // read/write assertions for register: prio25 - `ASSERT(prio25_wr_A, wr_P(2, 9'h6c, i_rv_plic.reg2hw.prio25.q, 0), clk_i, !rst_ni) - `ASSERT(prio25_rd_A, rd_P(2, 9'h6c, i_rv_plic.reg2hw.prio25.q), clk_i, !rst_ni) + `ASSERT(prio25_wr_A, wr_P(2, 9'h6c, i_rv_plic.reg2hw.prio25.q, 0)) + `ASSERT(prio25_rd_A, rd_P(2, 9'h6c, i_rv_plic.reg2hw.prio25.q)) // read/write assertions for register: prio26 - `ASSERT(prio26_wr_A, wr_P(2, 9'h70, i_rv_plic.reg2hw.prio26.q, 0), clk_i, !rst_ni) - `ASSERT(prio26_rd_A, rd_P(2, 9'h70, i_rv_plic.reg2hw.prio26.q), clk_i, !rst_ni) + `ASSERT(prio26_wr_A, wr_P(2, 9'h70, i_rv_plic.reg2hw.prio26.q, 0)) + `ASSERT(prio26_rd_A, rd_P(2, 9'h70, i_rv_plic.reg2hw.prio26.q)) // read/write assertions for register: prio27 - `ASSERT(prio27_wr_A, wr_P(2, 9'h74, i_rv_plic.reg2hw.prio27.q, 0), clk_i, !rst_ni) - `ASSERT(prio27_rd_A, rd_P(2, 9'h74, i_rv_plic.reg2hw.prio27.q), clk_i, !rst_ni) + `ASSERT(prio27_wr_A, wr_P(2, 9'h74, i_rv_plic.reg2hw.prio27.q, 0)) + `ASSERT(prio27_rd_A, rd_P(2, 9'h74, i_rv_plic.reg2hw.prio27.q)) // read/write assertions for register: prio28 - `ASSERT(prio28_wr_A, wr_P(2, 9'h78, i_rv_plic.reg2hw.prio28.q, 0), clk_i, !rst_ni) - `ASSERT(prio28_rd_A, rd_P(2, 9'h78, i_rv_plic.reg2hw.prio28.q), clk_i, !rst_ni) + `ASSERT(prio28_wr_A, wr_P(2, 9'h78, i_rv_plic.reg2hw.prio28.q, 0)) + `ASSERT(prio28_rd_A, rd_P(2, 9'h78, i_rv_plic.reg2hw.prio28.q)) // read/write assertions for register: prio29 - `ASSERT(prio29_wr_A, wr_P(2, 9'h7c, i_rv_plic.reg2hw.prio29.q, 0), clk_i, !rst_ni) - `ASSERT(prio29_rd_A, rd_P(2, 9'h7c, i_rv_plic.reg2hw.prio29.q), clk_i, !rst_ni) + `ASSERT(prio29_wr_A, wr_P(2, 9'h7c, i_rv_plic.reg2hw.prio29.q, 0)) + `ASSERT(prio29_rd_A, rd_P(2, 9'h7c, i_rv_plic.reg2hw.prio29.q)) // read/write assertions for register: prio30 - `ASSERT(prio30_wr_A, wr_P(2, 9'h80, i_rv_plic.reg2hw.prio30.q, 0), clk_i, !rst_ni) - `ASSERT(prio30_rd_A, rd_P(2, 9'h80, i_rv_plic.reg2hw.prio30.q), clk_i, !rst_ni) + `ASSERT(prio30_wr_A, wr_P(2, 9'h80, i_rv_plic.reg2hw.prio30.q, 0)) + `ASSERT(prio30_rd_A, rd_P(2, 9'h80, i_rv_plic.reg2hw.prio30.q)) // read/write assertions for register: prio31 - `ASSERT(prio31_wr_A, wr_P(2, 9'h84, i_rv_plic.reg2hw.prio31.q, 0), clk_i, !rst_ni) - `ASSERT(prio31_rd_A, rd_P(2, 9'h84, i_rv_plic.reg2hw.prio31.q), clk_i, !rst_ni) + `ASSERT(prio31_wr_A, wr_P(2, 9'h84, i_rv_plic.reg2hw.prio31.q, 0)) + `ASSERT(prio31_rd_A, rd_P(2, 9'h84, i_rv_plic.reg2hw.prio31.q)) // define local fpv variable for the multi_reg logic [31:0] ie0_q_fpv; @@ -230,19 +230,19 @@ end // read/write assertions for register: ie0 - `ASSERT(ie0_wr_A, wr_P(31, 9'h100, ie0_q_fpv[31:0], 0), clk_i, !rst_ni) - `ASSERT(ie0_rd_A, rd_P(31, 9'h100, ie0_q_fpv[31:0]), clk_i, !rst_ni) + `ASSERT(ie0_wr_A, wr_P(31, 9'h100, ie0_q_fpv[31:0], 0)) + `ASSERT(ie0_rd_A, rd_P(31, 9'h100, ie0_q_fpv[31:0])) // read/write assertions for register: threshold0 - `ASSERT(threshold0_wr_A, wr_P(2, 9'h104, i_rv_plic.reg2hw.threshold0.q, 0), clk_i, !rst_ni) - `ASSERT(threshold0_rd_A, rd_P(2, 9'h104, i_rv_plic.reg2hw.threshold0.q), clk_i, !rst_ni) + `ASSERT(threshold0_wr_A, wr_P(2, 9'h104, i_rv_plic.reg2hw.threshold0.q, 0)) + `ASSERT(threshold0_rd_A, rd_P(2, 9'h104, i_rv_plic.reg2hw.threshold0.q)) // read/write assertions for register: cc0 - `ASSERT(cc0_wr_A, wr_ext_P(5, 9'h108, i_rv_plic.reg2hw.cc0.q, 0), clk_i, !rst_ni) - `ASSERT(cc0_rd_A, rd_ext_P(5, 9'h108, i_rv_plic.hw2reg.cc0.d), clk_i, !rst_ni) + `ASSERT(cc0_wr_A, wr_ext_P(5, 9'h108, i_rv_plic.reg2hw.cc0.q, 0)) + `ASSERT(cc0_rd_A, rd_ext_P(5, 9'h108, i_rv_plic.hw2reg.cc0.d)) // read/write assertions for register: msip0 - `ASSERT(msip0_wr_A, wr_P(0, 9'h10c, i_rv_plic.reg2hw.msip0.q, 0), clk_i, !rst_ni) - `ASSERT(msip0_rd_A, rd_P(0, 9'h10c, i_rv_plic.reg2hw.msip0.q), clk_i, !rst_ni) + `ASSERT(msip0_wr_A, wr_P(0, 9'h10c, i_rv_plic.reg2hw.msip0.q, 0)) + `ASSERT(msip0_rd_A, rd_P(0, 9'h10c, i_rv_plic.reg2hw.msip0.q)) endmodule
diff --git a/hw/ip/rv_plic/rtl/rv_plic.sv b/hw/ip/rv_plic/rtl/rv_plic.sv index 3cac286..a5aae45 100644 --- a/hw/ip/rv_plic/rtl/rv_plic.sv +++ b/hw/ip/rv_plic/rtl/rv_plic.sv
@@ -80,12 +80,12 @@ end end - //`ASSERT_PULSE(claimPulse, claim_re[i], clk_i, !rst_ni) - //`ASSERT_PULSE(completePulse, complete_we[i], clk_i, !rst_ni) + //`ASSERT_PULSE(claimPulse, claim_re[i]) + //`ASSERT_PULSE(completePulse, complete_we[i]) - `ASSERT(onehot0Claim, $onehot0(claim_re), clk_i, !rst_ni) + `ASSERT(onehot0Claim, $onehot0(claim_re)) - `ASSERT(onehot0Complete, $onehot0(complete_we), clk_i, !rst_ni) + `ASSERT(onehot0Complete, $onehot0(complete_we)) ////////////// // Priority // @@ -224,12 +224,12 @@ ); // Assertions - `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid, clk_i, !rst_ni) - `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready, clk_i, !rst_ni) - `ASSERT_KNOWN(IrqKnownO_A, irq_o, clk_i, !rst_ni) - `ASSERT_KNOWN(MsipKnownO_A, msip_o, clk_i, !rst_ni) + `ASSERT_KNOWN(TlDValidKnownO_A, tl_o.d_valid) + `ASSERT_KNOWN(TlAReadyKnownO_A, tl_o.a_ready) + `ASSERT_KNOWN(IrqKnownO_A, irq_o) + `ASSERT_KNOWN(MsipKnownO_A, msip_o) for (genvar k = 0; k < NumTarget; k++) begin : gen_irq_id_known - `ASSERT_KNOWN(IrqIdKnownO_A, irq_id_o[k], clk_i, !rst_ni) + `ASSERT_KNOWN(IrqIdKnownO_A, irq_id_o[k]) end endmodule
diff --git a/hw/ip/rv_plic/rtl/rv_plic_reg_top.sv b/hw/ip/rv_plic/rtl/rv_plic_reg_top.sv index 9bf5e26..fb8fff7 100644 --- a/hw/ip/rv_plic/rtl/rv_plic_reg_top.sv +++ b/hw/ip/rv_plic/rtl/rv_plic_reg_top.sv
@@ -4492,15 +4492,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/rv_timer/rtl/rv_timer.sv b/hw/ip/rv_timer/rtl/rv_timer.sv index 698b2f2..7602960 100644 --- a/hw/ip/rv_timer/rtl/rv_timer.sv +++ b/hw/ip/rv_timer/rtl/rv_timer.sv
@@ -124,8 +124,8 @@ //////////////// // Assertions // //////////////// - `ASSERT_KNOWN(TlODValidKnown, tl_o.d_valid, clk_i, !rst_ni) - `ASSERT_KNOWN(TlOAReadyKnown, tl_o.a_ready, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrTimerExpired00Known, intr_timer_expired_0_0_o, clk_i, !rst_ni) + `ASSERT_KNOWN(TlODValidKnown, tl_o.d_valid) + `ASSERT_KNOWN(TlOAReadyKnown, tl_o.a_ready) + `ASSERT_KNOWN(IntrTimerExpired00Known, intr_timer_expired_0_0_o) endmodule
diff --git a/hw/ip/rv_timer/rtl/rv_timer_reg_top.sv b/hw/ip/rv_timer/rtl/rv_timer_reg_top.sv index 8e0f108..de5c20e 100644 --- a/hw/ip/rv_timer/rtl/rv_timer_reg_top.sv +++ b/hw/ip/rv_timer/rtl/rv_timer_reg_top.sv
@@ -479,15 +479,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/spi_device/rtl/spi_device.sv b/hw/ip/spi_device/rtl/spi_device.sv index 645546d..4937369 100644 --- a/hw/ip/spi_device/rtl/spi_device.sv +++ b/hw/ip/spi_device/rtl/spi_device.sv
@@ -564,13 +564,13 @@ // make sure scanmode_i is never X (including during reset) `ASSERT_KNOWN(scanmodeKnown, scanmode_i, clk_i, 0) - `ASSERT_KNOWN(CioMisoEnOKnown, cio_miso_en_o, clk_i, !rst_ni) + `ASSERT_KNOWN(CioMisoEnOKnown, cio_miso_en_o) - `ASSERT_KNOWN(IntrRxfOKnown, intr_rxf_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrRxlvlOKnown, intr_rxlvl_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrTxlvlOKnown, intr_txlvl_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrRxerrOKnown, intr_rxerr_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrRxoverflowOKnown, intr_rxoverflow_o, clk_i, !rst_ni) - `ASSERT_KNOWN(IntrTxunderflowOKnown, intr_txunderflow_o, clk_i, !rst_ni) + `ASSERT_KNOWN(IntrRxfOKnown, intr_rxf_o ) + `ASSERT_KNOWN(IntrRxlvlOKnown, intr_rxlvl_o ) + `ASSERT_KNOWN(IntrTxlvlOKnown, intr_txlvl_o ) + `ASSERT_KNOWN(IntrRxerrOKnown, intr_rxerr_o ) + `ASSERT_KNOWN(IntrRxoverflowOKnown, intr_rxoverflow_o ) + `ASSERT_KNOWN(IntrTxunderflowOKnown, intr_txunderflow_o) endmodule
diff --git a/hw/ip/spi_device/rtl/spi_device_reg_top.sv b/hw/ip/spi_device/rtl/spi_device_reg_top.sv index b230038..a450513 100644 --- a/hw/ip/spi_device/rtl/spi_device_reg_top.sv +++ b/hw/ip/spi_device/rtl/spi_device_reg_top.sv
@@ -1527,15 +1527,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/tlul/rtl/sram2tlul.sv b/hw/ip/tlul/rtl/sram2tlul.sv index 67c8084..2deb7f5 100644 --- a/hw/ip/tlul/rtl/sram2tlul.sv +++ b/hw/ip/tlul/rtl/sram2tlul.sv
@@ -57,6 +57,6 @@ // below assertion fails when TL-UL doesn't accept request in a cycle, // which is currently not supported by sram2tlul - `ASSERT(validNotReady, tl_o.a_valid |-> tl_i.a_ready, clk_i, !rst_ni) + `ASSERT(validNotReady, tl_o.a_valid |-> tl_i.a_ready) endmodule
diff --git a/hw/ip/tlul/rtl/tlul_adapter_sram.sv b/hw/ip/tlul/rtl/tlul_adapter_sram.sv index e4cdbfa..56e0c78 100644 --- a/hw/ip/tlul/rtl/tlul_adapter_sram.sv +++ b/hw/ip/tlul/rtl/tlul_adapter_sram.sv
@@ -264,21 +264,21 @@ ); // below assertion fails when SRAM rvalid is asserted even though ReqFifo is empty - `ASSERT(rvalidHighReqFifoEmpty, rvalid_i |-> reqfifo_rvalid, clk_i, !rst_ni) + `ASSERT(rvalidHighReqFifoEmpty, rvalid_i |-> reqfifo_rvalid) // below assertion fails when outstanding value is too small (SRAM rvalid is asserted // even though the RspFifo is full) - `ASSERT(rvalidHighWhenRspFifoFull, rvalid_i |-> rspfifo_wready, clk_i, !rst_ni) + `ASSERT(rvalidHighWhenRspFifoFull, rvalid_i |-> rspfifo_wready) // If both ErrOnWrite and ErrOnRead are set, this block is useless `ASSERT_INIT(adapterNoReadOrWrite, (ErrOnWrite & ErrOnRead) == 0) // make sure outputs are defined - `ASSERT_KNOWN(TlOutKnown_A, tl_o, clk_i, !rst_ni) - `ASSERT_KNOWN(ReqOutKnown_A, req_o, clk_i, !rst_ni) - `ASSERT_KNOWN(WeOutKnown_A, we_o, clk_i, !rst_ni) - `ASSERT_KNOWN(AddrOutKnown_A, addr_o, clk_i, !rst_ni) - `ASSERT_KNOWN(WdataOutKnown_A, wdata_o, clk_i, !rst_ni) - `ASSERT_KNOWN(WmaskOutKnown_A, wmask_o, clk_i, !rst_ni) + `ASSERT_KNOWN(TlOutKnown_A, tl_o ) + `ASSERT_KNOWN(ReqOutKnown_A, req_o ) + `ASSERT_KNOWN(WeOutKnown_A, we_o ) + `ASSERT_KNOWN(AddrOutKnown_A, addr_o ) + `ASSERT_KNOWN(WdataOutKnown_A, wdata_o) + `ASSERT_KNOWN(WmaskOutKnown_A, wmask_o) endmodule
diff --git a/hw/ip/tlul/rtl/tlul_assert.sv b/hw/ip/tlul/rtl/tlul_assert.sv index b34b188..a27c80a 100644 --- a/hw/ip/tlul/rtl/tlul_assert.sv +++ b/hw/ip/tlul/rtl/tlul_assert.sv
@@ -273,16 +273,15 @@ // a_* should be known when a_valid == 1 (a_opcode and a_param are already covered above) // This also covers ASSERT_KNOWN of a_valid `ASSERT_VALID_DATA(aKnown_A, h2d.a_valid, {h2d.a_size, h2d.a_source, h2d.a_address, - h2d.a_mask, h2d.a_user}, clk_i, !rst_ni) + h2d.a_mask, h2d.a_user}) // d_* should be known when d_valid == 1 (d_opcode, d_param, d_size already covered above) // This also covers ASSERT_KNOWN of d_valid - `ASSERT_VALID_DATA(dKnown_A, d2h.d_valid, {d2h.d_source, d2h.d_sink, d2h.d_error, d2h.d_user}, - clk_i, !rst_ni) + `ASSERT_VALID_DATA(dKnown_A, d2h.d_valid, {d2h.d_source, d2h.d_sink, d2h.d_error, d2h.d_user}) // make sure ready is not X after reset - `ASSERT_KNOWN(aReadyKnown_A, d2h.a_ready, clk_i, !rst_ni) - `ASSERT_KNOWN(dReadyKnown_A, h2d.d_ready, clk_i, !rst_ni) + `ASSERT_KNOWN(aReadyKnown_A, d2h.a_ready) + `ASSERT_KNOWN(dReadyKnown_A, h2d.d_ready) `endif `endif endmodule : tlul_assert
diff --git a/hw/ip/tlul/rtl/tlul_socket_m1.sv b/hw/ip/tlul/rtl/tlul_socket_m1.sv index 5bace6a..8637ad2 100644 --- a/hw/ip/tlul/rtl/tlul_socket_m1.sv +++ b/hw/ip/tlul/rtl/tlul_socket_m1.sv
@@ -98,7 +98,7 @@ reqid_sub }; - `ASSERT(idInRange, tl_h_i[i].a_valid |-> tl_h_i[i].a_source[IDW-1 -:STIDW] == '0, clk_i, !rst_ni) + `ASSERT(idInRange, tl_h_i[i].a_valid |-> tl_h_i[i].a_source[IDW-1 -:STIDW] == '0) // assign not connected bits to nc_* signal to make lint happy logic [IDW-1 : IDW-STIDW] unused_tl_h_source; @@ -253,6 +253,6 @@ // this assertion fails when rspid[0+:STIDW] not in [0..M-1] `ASSERT(rspIdInRange, drsp_fifo_o.d_valid |-> - drsp_fifo_o.d_source[0+:STIDW] >= 0 && drsp_fifo_o.d_source[0+:STIDW] < M, clk_i, !rst_ni) + drsp_fifo_o.d_source[0+:STIDW] >= 0 && drsp_fifo_o.d_source[0+:STIDW] < M) endmodule
diff --git a/hw/ip/trial1/rtl/trial1_reg_top.sv b/hw/ip/trial1/rtl/trial1_reg_top.sv index 81a3dbe..bdc8f5d 100644 --- a/hw/ip/trial1/rtl/trial1_reg_top.sv +++ b/hw/ip/trial1/rtl/trial1_reg_top.sv
@@ -1261,15 +1261,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/uart/rtl/uart.sv b/hw/ip/uart/rtl/uart.sv index 703be73..536bf80 100644 --- a/hw/ip/uart/rtl/uart.sv +++ b/hw/ip/uart/rtl/uart.sv
@@ -69,17 +69,17 @@ assign cio_tx_en_o = 1'b1; // Assert Known for outputs - `ASSERT_KNOWN(txenKnown, cio_tx_en_o, clk_i, !rst_ni) + `ASSERT_KNOWN(txenKnown, cio_tx_en_o) `ASSERT_KNOWN(txKnown, cio_tx_o, clk_i, !rst_ni || !cio_tx_en_o) // Assert Known for interrupts - `ASSERT_KNOWN(txWatermarkKnown, intr_tx_watermark_o, clk_i, !rst_ni) - `ASSERT_KNOWN(rxWatermarkKnown, intr_rx_watermark_o, clk_i, !rst_ni) - `ASSERT_KNOWN(txEmptyKnown, intr_tx_empty_o, clk_i, !rst_ni) - `ASSERT_KNOWN(rxOverflowKnown, intr_rx_overflow_o, clk_i, !rst_ni) - `ASSERT_KNOWN(rxFrameErrKnown, intr_rx_frame_err_o, clk_i, !rst_ni) - `ASSERT_KNOWN(rxBreakErrKnown, intr_rx_break_err_o, clk_i, !rst_ni) - `ASSERT_KNOWN(rxTimeoutKnown, intr_rx_timeout_o, clk_i, !rst_ni) - `ASSERT_KNOWN(rxParityErrKnown, intr_rx_parity_err_o, clk_i, !rst_ni) + `ASSERT_KNOWN(txWatermarkKnown, intr_tx_watermark_o) + `ASSERT_KNOWN(rxWatermarkKnown, intr_rx_watermark_o) + `ASSERT_KNOWN(txEmptyKnown, intr_tx_empty_o) + `ASSERT_KNOWN(rxOverflowKnown, intr_rx_overflow_o) + `ASSERT_KNOWN(rxFrameErrKnown, intr_rx_frame_err_o) + `ASSERT_KNOWN(rxBreakErrKnown, intr_rx_break_err_o) + `ASSERT_KNOWN(rxTimeoutKnown, intr_rx_timeout_o) + `ASSERT_KNOWN(rxParityErrKnown, intr_rx_parity_err_o) endmodule
diff --git a/hw/ip/uart/rtl/uart_reg_top.sv b/hw/ip/uart/rtl/uart_reg_top.sv index a176846..f25d459 100644 --- a/hw/ip/uart/rtl/uart_reg_top.sv +++ b/hw/ip/uart/rtl/uart_reg_top.sv
@@ -1663,15 +1663,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/usbdev/rtl/usbdev_reg_top.sv b/hw/ip/usbdev/rtl/usbdev_reg_top.sv index 89ea83d..afd2600 100644 --- a/hw/ip/usbdev/rtl/usbdev_reg_top.sv +++ b/hw/ip/usbdev/rtl/usbdev_reg_top.sv
@@ -6187,15 +6187,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/hw/ip/usbuart/rtl/usbuart_reg_top.sv b/hw/ip/usbuart/rtl/usbuart_reg_top.sv index 3275bb6..4c2d6e2 100644 --- a/hw/ip/usbuart/rtl/usbuart_reg_top.sv +++ b/hw/ip/usbuart/rtl/usbuart_reg_top.sv
@@ -1801,15 +1801,15 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule
diff --git a/util/fpvgen/assert_fpv.sv.tpl b/util/fpvgen/assert_fpv.sv.tpl index 14ebc22..82b2a41 100644 --- a/util/fpvgen/assert_fpv.sv.tpl +++ b/util/fpvgen/assert_fpv.sv.tpl
@@ -43,18 +43,18 @@ // Assumptions // ///////////////// - // `ASSUME(MyAssumption_M, ..., clk_i, !rst_ni) + // `ASSUME(MyAssumption_M, ...) //////////////////////// // Forward Assertions // //////////////////////// - // `ASSERT(MyFwdAssertion_A, ..., clk_i, !rst_ni) + // `ASSERT(MyFwdAssertion_A, ...) ///////////////////////// // Backward Assertions // ///////////////////////// - // `ASSERT(MyBkwdAssertion_A, ..., clk_i, !rst_ni) + // `ASSERT(MyBkwdAssertion_A, ...) endmodule : ${dut.name}_assert_fpv
diff --git a/util/reggen/fpv_csr.sv.tpl b/util/reggen/fpv_csr.sv.tpl index 4ceefa5..ab5603c 100644 --- a/util/reggen/fpv_csr.sv.tpl +++ b/util/reggen/fpv_csr.sv.tpl
@@ -177,21 +177,21 @@ // read/write assertions for register: ${reg_name} % if reg_flat.dvrights in {"RW", "WO"}: % if reg_flat.get_n_bits(["q", "d"]) == 0: - `ASSERT(${reg_name}_wr_A, ${wr_prperty}(${reg_msb}, ${reg_offset}, ${reg_we_path}, ${reg_wen}), clk_i, !rst_ni) + `ASSERT(${reg_name}_wr_A, ${wr_prperty}(${reg_msb}, ${reg_offset}, ${reg_we_path}, ${reg_wen})) % else: - `ASSERT(${reg_name}_wr_A, ${wr_prperty}(${reg_msb}, ${reg_offset}, ${reg_q_path}, ${reg_wen}), clk_i, !rst_ni) + `ASSERT(${reg_name}_wr_A, ${wr_prperty}(${reg_msb}, ${reg_offset}, ${reg_q_path}, ${reg_wen})) % endif % if regwen: - `ASSERT(${reg_name}_stable_A, wr_regen_stable_P(${reg_wen}, ${reg_q_path}), clk_i, !rst_ni) + `ASSERT(${reg_name}_stable_A, wr_regen_stable_P(${reg_wen}, ${reg_q_path})) % endif % endif % if reg_flat.dvrights in {"RW", "RO"}: % if reg_flat.get_n_bits(["q", "d"]) == 0: - `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_msb}, ${reg_offset}, ${reg_qs_path}), clk_i, !rst_ni) + `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_msb}, ${reg_offset}, ${reg_qs_path})) % elif reg_flat.get_n_bits(["d"]): - `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_msb}, ${reg_offset}, ${reg_d_path}), clk_i, !rst_ni) + `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_msb}, ${reg_offset}, ${reg_d_path})) % elif reg_flat.get_n_bits(["q"]) and (r.ishomog or ((not r.ishomog) and r.get_fields_flat()[0].get_n_bits(["q"]))): - `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_msb}, ${reg_offset}, ${reg_q_path}), clk_i, !rst_ni) + `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_msb}, ${reg_offset}, ${reg_q_path})) % endif % endif % endfor
diff --git a/util/reggen/reg_top.sv.tpl b/util/reggen/reg_top.sv.tpl index 08f9ad7..bb689db 100644 --- a/util/reggen/reg_top.sv.tpl +++ b/util/reggen/reg_top.sv.tpl
@@ -369,16 +369,16 @@ end // Assertions for Register Interface - `ASSERT_PULSE(wePulse, reg_we, clk_i, !rst_ni) - `ASSERT_PULSE(rePulse, reg_re, clk_i, !rst_ni) + `ASSERT_PULSE(wePulse, reg_we) + `ASSERT_PULSE(rePulse, reg_re) - `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid, clk_i, !rst_ni) + `ASSERT(reAfterRv, $rose(reg_re || reg_we) |=> tl_o.d_valid) - `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) + `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit)) // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) endmodule <%def name="str_bits_sv(msb, lsb)">\