[hw] Add default clk/rst for prim_assert macros Fixes #1259 Signed-off-by: Greg Chadwick <gac@lowrisc.org>
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