[prim_mubi] Fix sampling issue in MUBI sync assertions
Fix #15234
Signed-off-by: Michael Schaffner <msf@google.com>
diff --git a/hw/ip/prim/rtl/prim_lc_sync.sv b/hw/ip/prim/rtl/prim_lc_sync.sv
index ccfd748..7293135 100644
--- a/hw/ip/prim/rtl/prim_lc_sync.sv
+++ b/hw/ip/prim/rtl/prim_lc_sync.sv
@@ -46,13 +46,29 @@
.d_i(lc_en_i),
.q_o(lc_en)
);
- // Without the sampled rst_ni pre-condition, this may cause false assertion failures
- // right after a reset release, since the "iff disable" condition with the rst_ni is
- // sampled in the "observed" SV scheduler region after all assignments have been
- // evaluated. This is a simulation artifact due to reset synchronization in RTL, which
- // releases rst_ni on the active clock edge. This causes the assertion to evaluate
- // although the reset was actually 0 when entering this simulation cycle.
- `ASSERT(OutputDelay_A, rst_ni |-> ##2 lc_en_o == {NumCopies{$past(lc_en_i, 2)}})
+
+// Note regarding SVA below:
+//
+// 1) Without the sampled rst_ni pre-condition, this may cause false assertion failures right after
+// a reset release, since the "disable iff" condition with the rst_ni is sampled in the "observed"
+// SV scheduler region after all assignments have been evaluated (see also LRM section 16.12, page
+// 423). This is a simulation artifact due to reset synchronization in RTL, which releases rst_ni
+// on the active clock edge. This causes the assertion to evaluate although the reset was actually
+// 0 when entering this simulation cycle.
+//
+// 2) Similarly to 1) there can be sampling mismatches of the lc_en_i signal since that signal may
+// originate from a different clock domain. I.e., in cases where the lc_en_i signal changes exactly
+// at the same time that the clk_i signal rises, the SVA will not pick up that change in that clock
+// cycle, whereas RTL will because SVAs sample values in the "preponed" region. To that end we make
+// use of an RTL helper variable to sample the lc_en_i signal, hence ensuring that there are no
+// sampling mismatches.
+`ifdef INC_ASSERT
+ lc_ctrl_pkg::lc_tx_t lc_en_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ lc_en_in_sva_q <= lc_en_i;
+ end
+ `ASSERT(OutputDelay_A, rst_ni |-> ##2 lc_en_o == {NumCopies{$past(lc_en_in_sva_q, 1)}})
+`endif
end else begin : gen_no_flops
// This unused companion logic helps remove lint errors
// for modules where clock and reset are used for assertions only
diff --git a/hw/ip/prim/rtl/prim_mubi12_sync.sv b/hw/ip/prim/rtl/prim_mubi12_sync.sv
index a48b3ed..19605fe 100644
--- a/hw/ip/prim/rtl/prim_mubi12_sync.sv
+++ b/hw/ip/prim/rtl/prim_mubi12_sync.sv
@@ -101,17 +101,39 @@
);
end
+// Note regarding SVAs below:
+//
+// 1) Without the sampled rst_ni pre-condition, this may cause false assertion failures right after
+// a reset release, since the "disable iff" condition with the rst_ni is sampled in the "observed"
+// SV scheduler region after all assignments have been evaluated (see also LRM section 16.12, page
+// 423). This is a simulation artifact due to reset synchronization in RTL, which releases rst_ni
+// on the active clock edge. This causes the assertion to evaluate although the reset was actually
+// 0 when entering this simulation cycle.
+//
+// 2) Similarly to 1) there can be sampling mismatches of the lc_en_i signal since that signal may
+// originate from a different clock domain. I.e., in cases where the lc_en_i signal changes exactly
+// at the same time that the clk_i signal rises, the SVA will not pick up that change in that clock
+// cycle, whereas RTL will because SVAs sample values in the "preponed" region. To that end we make
+// use of an RTL helper variable to sample the lc_en_i signal, hence ensuring that there are no
+// sampling mismatches.
+`ifdef INC_ASSERT
+ mubi12_t mubi_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ mubi_in_sva_q <= mubi_i;
+ end
`ASSERT(OutputIfUnstable_A, sig_unstable |-> mubi_o == {NumCopies{reset_value}})
- `ASSERT(OutputDelay_A, ##3 !sig_unstable |-> mubi_o == {NumCopies{$past(mubi_i, 3)}})
+ `ASSERT(OutputDelay_A, rst_ni |-> ##3 sig_unstable ||
+ mubi_o == {NumCopies{$past(mubi_in_sva_q, 2)}})
+`endif
end else begin : gen_no_stable_chks
assign mubi = mubi_sync;
- // Without the sampled rst_ni pre-condition, this may cause false assertion failures
- // right after a reset release, since the "iff disable" condition with the rst_ni is
- // sampled in the "observed" SV scheduler region after all assignments have been
- // evaluated. This is a simulation artifact due to reset synchronization in RTL, which
- // releases rst_ni on the active clock edge. This causes the assertion to evaluate
- // although the reset was actually 0 when entering this simulation cycle.
- `ASSERT(OutputDelay_A, rst_ni |-> ##2 mubi_o == {NumCopies{$past(mubi_i, 2)}})
+`ifdef INC_ASSERT
+ mubi12_t mubi_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ mubi_in_sva_q <= mubi_i;
+ end
+ `ASSERT(OutputDelay_A, rst_ni |-> ##2 mubi_o == {NumCopies{$past(mubi_in_sva_q, 1)}})
+`endif
end
end else begin : gen_no_flops
diff --git a/hw/ip/prim/rtl/prim_mubi16_sync.sv b/hw/ip/prim/rtl/prim_mubi16_sync.sv
index c510f10..24b400e 100644
--- a/hw/ip/prim/rtl/prim_mubi16_sync.sv
+++ b/hw/ip/prim/rtl/prim_mubi16_sync.sv
@@ -101,17 +101,39 @@
);
end
+// Note regarding SVAs below:
+//
+// 1) Without the sampled rst_ni pre-condition, this may cause false assertion failures right after
+// a reset release, since the "disable iff" condition with the rst_ni is sampled in the "observed"
+// SV scheduler region after all assignments have been evaluated (see also LRM section 16.12, page
+// 423). This is a simulation artifact due to reset synchronization in RTL, which releases rst_ni
+// on the active clock edge. This causes the assertion to evaluate although the reset was actually
+// 0 when entering this simulation cycle.
+//
+// 2) Similarly to 1) there can be sampling mismatches of the lc_en_i signal since that signal may
+// originate from a different clock domain. I.e., in cases where the lc_en_i signal changes exactly
+// at the same time that the clk_i signal rises, the SVA will not pick up that change in that clock
+// cycle, whereas RTL will because SVAs sample values in the "preponed" region. To that end we make
+// use of an RTL helper variable to sample the lc_en_i signal, hence ensuring that there are no
+// sampling mismatches.
+`ifdef INC_ASSERT
+ mubi16_t mubi_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ mubi_in_sva_q <= mubi_i;
+ end
`ASSERT(OutputIfUnstable_A, sig_unstable |-> mubi_o == {NumCopies{reset_value}})
- `ASSERT(OutputDelay_A, ##3 !sig_unstable |-> mubi_o == {NumCopies{$past(mubi_i, 3)}})
+ `ASSERT(OutputDelay_A, rst_ni |-> ##3 sig_unstable ||
+ mubi_o == {NumCopies{$past(mubi_in_sva_q, 2)}})
+`endif
end else begin : gen_no_stable_chks
assign mubi = mubi_sync;
- // Without the sampled rst_ni pre-condition, this may cause false assertion failures
- // right after a reset release, since the "iff disable" condition with the rst_ni is
- // sampled in the "observed" SV scheduler region after all assignments have been
- // evaluated. This is a simulation artifact due to reset synchronization in RTL, which
- // releases rst_ni on the active clock edge. This causes the assertion to evaluate
- // although the reset was actually 0 when entering this simulation cycle.
- `ASSERT(OutputDelay_A, rst_ni |-> ##2 mubi_o == {NumCopies{$past(mubi_i, 2)}})
+`ifdef INC_ASSERT
+ mubi16_t mubi_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ mubi_in_sva_q <= mubi_i;
+ end
+ `ASSERT(OutputDelay_A, rst_ni |-> ##2 mubi_o == {NumCopies{$past(mubi_in_sva_q, 1)}})
+`endif
end
end else begin : gen_no_flops
diff --git a/hw/ip/prim/rtl/prim_mubi4_sync.sv b/hw/ip/prim/rtl/prim_mubi4_sync.sv
index 3834395..584c357 100644
--- a/hw/ip/prim/rtl/prim_mubi4_sync.sv
+++ b/hw/ip/prim/rtl/prim_mubi4_sync.sv
@@ -101,17 +101,39 @@
);
end
+// Note regarding SVAs below:
+//
+// 1) Without the sampled rst_ni pre-condition, this may cause false assertion failures right after
+// a reset release, since the "disable iff" condition with the rst_ni is sampled in the "observed"
+// SV scheduler region after all assignments have been evaluated (see also LRM section 16.12, page
+// 423). This is a simulation artifact due to reset synchronization in RTL, which releases rst_ni
+// on the active clock edge. This causes the assertion to evaluate although the reset was actually
+// 0 when entering this simulation cycle.
+//
+// 2) Similarly to 1) there can be sampling mismatches of the lc_en_i signal since that signal may
+// originate from a different clock domain. I.e., in cases where the lc_en_i signal changes exactly
+// at the same time that the clk_i signal rises, the SVA will not pick up that change in that clock
+// cycle, whereas RTL will because SVAs sample values in the "preponed" region. To that end we make
+// use of an RTL helper variable to sample the lc_en_i signal, hence ensuring that there are no
+// sampling mismatches.
+`ifdef INC_ASSERT
+ mubi4_t mubi_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ mubi_in_sva_q <= mubi_i;
+ end
`ASSERT(OutputIfUnstable_A, sig_unstable |-> mubi_o == {NumCopies{reset_value}})
- `ASSERT(OutputDelay_A, ##3 !sig_unstable |-> mubi_o == {NumCopies{$past(mubi_i, 3)}})
+ `ASSERT(OutputDelay_A, rst_ni |-> ##3 sig_unstable ||
+ mubi_o == {NumCopies{$past(mubi_in_sva_q, 2)}})
+`endif
end else begin : gen_no_stable_chks
assign mubi = mubi_sync;
- // Without the sampled rst_ni pre-condition, this may cause false assertion failures
- // right after a reset release, since the "iff disable" condition with the rst_ni is
- // sampled in the "observed" SV scheduler region after all assignments have been
- // evaluated. This is a simulation artifact due to reset synchronization in RTL, which
- // releases rst_ni on the active clock edge. This causes the assertion to evaluate
- // although the reset was actually 0 when entering this simulation cycle.
- `ASSERT(OutputDelay_A, rst_ni |-> ##2 mubi_o == {NumCopies{$past(mubi_i, 2)}})
+`ifdef INC_ASSERT
+ mubi4_t mubi_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ mubi_in_sva_q <= mubi_i;
+ end
+ `ASSERT(OutputDelay_A, rst_ni |-> ##2 mubi_o == {NumCopies{$past(mubi_in_sva_q, 1)}})
+`endif
end
end else begin : gen_no_flops
diff --git a/hw/ip/prim/rtl/prim_mubi8_sync.sv b/hw/ip/prim/rtl/prim_mubi8_sync.sv
index c626dd1..c0a4ffb 100644
--- a/hw/ip/prim/rtl/prim_mubi8_sync.sv
+++ b/hw/ip/prim/rtl/prim_mubi8_sync.sv
@@ -101,17 +101,39 @@
);
end
+// Note regarding SVAs below:
+//
+// 1) Without the sampled rst_ni pre-condition, this may cause false assertion failures right after
+// a reset release, since the "disable iff" condition with the rst_ni is sampled in the "observed"
+// SV scheduler region after all assignments have been evaluated (see also LRM section 16.12, page
+// 423). This is a simulation artifact due to reset synchronization in RTL, which releases rst_ni
+// on the active clock edge. This causes the assertion to evaluate although the reset was actually
+// 0 when entering this simulation cycle.
+//
+// 2) Similarly to 1) there can be sampling mismatches of the lc_en_i signal since that signal may
+// originate from a different clock domain. I.e., in cases where the lc_en_i signal changes exactly
+// at the same time that the clk_i signal rises, the SVA will not pick up that change in that clock
+// cycle, whereas RTL will because SVAs sample values in the "preponed" region. To that end we make
+// use of an RTL helper variable to sample the lc_en_i signal, hence ensuring that there are no
+// sampling mismatches.
+`ifdef INC_ASSERT
+ mubi8_t mubi_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ mubi_in_sva_q <= mubi_i;
+ end
`ASSERT(OutputIfUnstable_A, sig_unstable |-> mubi_o == {NumCopies{reset_value}})
- `ASSERT(OutputDelay_A, ##3 !sig_unstable |-> mubi_o == {NumCopies{$past(mubi_i, 3)}})
+ `ASSERT(OutputDelay_A, rst_ni |-> ##3 sig_unstable ||
+ mubi_o == {NumCopies{$past(mubi_in_sva_q, 2)}})
+`endif
end else begin : gen_no_stable_chks
assign mubi = mubi_sync;
- // Without the sampled rst_ni pre-condition, this may cause false assertion failures
- // right after a reset release, since the "iff disable" condition with the rst_ni is
- // sampled in the "observed" SV scheduler region after all assignments have been
- // evaluated. This is a simulation artifact due to reset synchronization in RTL, which
- // releases rst_ni on the active clock edge. This causes the assertion to evaluate
- // although the reset was actually 0 when entering this simulation cycle.
- `ASSERT(OutputDelay_A, rst_ni |-> ##2 mubi_o == {NumCopies{$past(mubi_i, 2)}})
+`ifdef INC_ASSERT
+ mubi8_t mubi_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ mubi_in_sva_q <= mubi_i;
+ end
+ `ASSERT(OutputDelay_A, rst_ni |-> ##2 mubi_o == {NumCopies{$past(mubi_in_sva_q, 1)}})
+`endif
end
end else begin : gen_no_flops
diff --git a/util/design/data/prim_mubi_sync.sv.tpl b/util/design/data/prim_mubi_sync.sv.tpl
index e5f8d52..3148c13 100644
--- a/util/design/data/prim_mubi_sync.sv.tpl
+++ b/util/design/data/prim_mubi_sync.sv.tpl
@@ -101,17 +101,39 @@
);
end
+// Note regarding SVAs below:
+//
+// 1) Without the sampled rst_ni pre-condition, this may cause false assertion failures right after
+// a reset release, since the "disable iff" condition with the rst_ni is sampled in the "observed"
+// SV scheduler region after all assignments have been evaluated (see also LRM section 16.12, page
+// 423). This is a simulation artifact due to reset synchronization in RTL, which releases rst_ni
+// on the active clock edge. This causes the assertion to evaluate although the reset was actually
+// 0 when entering this simulation cycle.
+//
+// 2) Similarly to 1) there can be sampling mismatches of the lc_en_i signal since that signal may
+// originate from a different clock domain. I.e., in cases where the lc_en_i signal changes exactly
+// at the same time that the clk_i signal rises, the SVA will not pick up that change in that clock
+// cycle, whereas RTL will because SVAs sample values in the "preponed" region. To that end we make
+// use of an RTL helper variable to sample the lc_en_i signal, hence ensuring that there are no
+// sampling mismatches.
+`ifdef INC_ASSERT
+ mubi${n_bits}_t mubi_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ mubi_in_sva_q <= mubi_i;
+ end
`ASSERT(OutputIfUnstable_A, sig_unstable |-> mubi_o == {NumCopies{reset_value}})
- `ASSERT(OutputDelay_A, ##3 !sig_unstable |-> mubi_o == {NumCopies{$past(mubi_i, 3)}})
+ `ASSERT(OutputDelay_A, rst_ni |-> ##3 sig_unstable ||
+ mubi_o == {NumCopies{$past(mubi_in_sva_q, 2)}})
+`endif
end else begin : gen_no_stable_chks
assign mubi = mubi_sync;
- // Without the sampled rst_ni pre-condition, this may cause false assertion failures
- // right after a reset release, since the "iff disable" condition with the rst_ni is
- // sampled in the "observed" SV scheduler region after all assignments have been
- // evaluated. This is a simulation artifact due to reset synchronization in RTL, which
- // releases rst_ni on the active clock edge. This causes the assertion to evaluate
- // although the reset was actually 0 when entering this simulation cycle.
- `ASSERT(OutputDelay_A, rst_ni |-> ##2 mubi_o == {NumCopies{$past(mubi_i, 2)}})
+`ifdef INC_ASSERT
+ mubi${n_bits}_t mubi_in_sva_q;
+ always_ff @(posedge clk_i) begin
+ mubi_in_sva_q <= mubi_i;
+ end
+ `ASSERT(OutputDelay_A, rst_ni |-> ##2 mubi_o == {NumCopies{$past(mubi_in_sva_q, 1)}})
+`endif
end
end else begin : gen_no_flops
