[dv] Add ASSERT_NET to check net value
Due to race condition described in #9017, can't use ASSERT_INIT to check
value of a net/logic.
Signed-off-by: Weicai Yang <weicai@google.com>
diff --git a/hw/ip/keymgr/rtl/keymgr.sv b/hw/ip/keymgr/rtl/keymgr.sv
index 0598965..6ada7dc 100644
--- a/hw/ip/keymgr/rtl/keymgr.sv
+++ b/hw/ip/keymgr/rtl/keymgr.sv
@@ -644,10 +644,7 @@
logic unused_kmac_en_masking;
assign unused_kmac_en_masking = kmac_en_masking_i;
- // Exclude this assertion check from FPV testbench to avoid compilation error
- `ifndef FPV_ON
- `ASSERT_INIT(KmacMaskCheck_A, KmacEnMasking == kmac_en_masking_i)
- `endif
+ `ASSERT_INIT_NET(KmacMaskCheck_A, KmacEnMasking == kmac_en_masking_i)
// Ensure all parameters are consistent
`ASSERT_INIT(FaultCntMatch_A, FaultLastPos == AsyncFaultLastIdx + SyncFaultLastIdx)
diff --git a/hw/ip/prim/rtl/prim_assert.sv b/hw/ip/prim/rtl/prim_assert.sv
index 1e484e5..da016e4 100644
--- a/hw/ip/prim/rtl/prim_assert.sv
+++ b/hw/ip/prim/rtl/prim_assert.sv
@@ -47,6 +47,8 @@
//
// ASSERT_INIT: Assertion in initial block. Can be used for things like parameter checking.
//
+// ASSERT_INIT_NET: Assertion in initial block. Can be used for initial value of a net.
+//
// ASSERT_FINAL: Assertion in final block. Can be used for things like queues being empty at end of
// sim, all credits returned at end of sim, state machines in idle at end of sim.
//
diff --git a/hw/ip/prim/rtl/prim_assert_dummy_macros.svh b/hw/ip/prim/rtl/prim_assert_dummy_macros.svh
index 4a0da70..0a71a33 100644
--- a/hw/ip/prim/rtl/prim_assert_dummy_macros.svh
+++ b/hw/ip/prim/rtl/prim_assert_dummy_macros.svh
@@ -7,6 +7,7 @@
`define ASSERT_I(__name, __prop)
`define ASSERT_INIT(__name, __prop)
+`define ASSERT_INIT_NET(__name, __prop)
`define ASSERT_FINAL(__name, __prop)
`define ASSERT(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST)
`define ASSERT_NEVER(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST)
diff --git a/hw/ip/prim/rtl/prim_assert_standard_macros.svh b/hw/ip/prim/rtl/prim_assert_standard_macros.svh
index 45415af..3042ffe 100644
--- a/hw/ip/prim/rtl/prim_assert_standard_macros.svh
+++ b/hw/ip/prim/rtl/prim_assert_standard_macros.svh
@@ -28,6 +28,18 @@
end \
`endif
+`define ASSERT_INIT_NET(__name, __prop) \
+ initial begin \
+ // When a net is assigned with a value, the assignment is evaluated after \
+ // initial in Xcelium. Add 1ps delay to check value after the assignment is \
+ // completed. \
+ #1ps; \
+ __name: assert (__prop) \
+ else begin \
+ `ASSERT_ERROR(__name) \
+ end \
+ end \
+
`define ASSERT_FINAL(__name, __prop) \
final begin \
__name: assert (__prop || $test$plusargs("disable_assert_final_checks")) \
diff --git a/hw/ip/prim/rtl/prim_assert_yosys_macros.svh b/hw/ip/prim/rtl/prim_assert_yosys_macros.svh
index f007e70..86f50b7 100644
--- a/hw/ip/prim/rtl/prim_assert_yosys_macros.svh
+++ b/hw/ip/prim/rtl/prim_assert_yosys_macros.svh
@@ -15,6 +15,11 @@
assert (__prop); \
end
+`define ASSERT_INIT_NET(__name, __prop) \
+ initial begin : __name \
+ #1ps assert (__prop); \
+ end
+
// This doesn't make much sense for a formal tool (we never get to the final block!)
`define ASSERT_FINAL(__name, __prop)
diff --git a/hw/ip/prim/rtl/prim_count.sv b/hw/ip/prim/rtl/prim_count.sv
index 20bb7f1..7fcbd95 100644
--- a/hw/ip/prim/rtl/prim_count.sv
+++ b/hw/ip/prim/rtl/prim_count.sv
@@ -216,10 +216,7 @@
`ifdef INC_ASSERT
logic unused_assert_connected;
- // ASSERT_INIT can only be used for paramters/constants in FPV.
- `ifdef SIMULATION
- `ASSERT_INIT(AssertConnected_A, unused_assert_connected === 1'b1 || !EnableAlertTriggerSVA)
- `endif
+ `ASSERT_INIT_NET(AssertConnected_A, unused_assert_connected === 1'b1 || !EnableAlertTriggerSVA)
`endif
endmodule // prim_count
diff --git a/hw/ip/prim/rtl/prim_sparse_fsm_flop.sv b/hw/ip/prim/rtl/prim_sparse_fsm_flop.sv
index d4bc13e..f3401a7 100644
--- a/hw/ip/prim/rtl/prim_sparse_fsm_flop.sv
+++ b/hw/ip/prim/rtl/prim_sparse_fsm_flop.sv
@@ -43,10 +43,7 @@
`ifdef INC_ASSERT
logic unused_assert_connected;
- // ASSERT_INIT can only be used for paramters/constants in FPV.
- `ifdef SIMULATION
- `ASSERT_INIT(AssertConnected_A, unused_assert_connected === 1'b1 || !EnableAlertTriggerSVA)
- `endif
+ `ASSERT_INIT_NET(AssertConnected_A, unused_assert_connected === 1'b1 || !EnableAlertTriggerSVA)
`endif
endmodule
