From 33f434a211cf3210346bd4450ba8b4d05521f45f Mon Sep 17 00:00:00 2001 From: Moritz Scherer Date: Wed, 15 Apr 2026 10:39:27 +0200 Subject: [PATCH] [NFC] Refine assertion to be robust to clk / rst event coincidence This patch fixes a reset glitch in the `lock_req` assertion. Previously, the assertion used `lock_d` as an antecedant of the assertion in the next cycle. Since IEEE 1800 does not guarantee the resolution of zero-delay updates, whenever the clock edge of `clk_i` coincides with the deassertion of `rst_ni` `lock_d` might be in any state, since it combinationally depends on inputs of the cache. This can lead to the assertion wrongfully triggering a cycle after reset. To fix this, this patch uses the latched `lock_q` an assumes the antecedant to hold in the same cycle instead. This leads to no functional changes, but avoids the zero-delay issue. --- src/multi_accept_rr_arb.sv | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/multi_accept_rr_arb.sv b/src/multi_accept_rr_arb.sv index 81d98a5..cd6ca06 100644 --- a/src/multi_accept_rr_arb.sv +++ b/src/multi_accept_rr_arb.sv @@ -65,10 +65,13 @@ module multi_accept_rr_arb #( )) else $fatal(1, "Lock implies same arbiter decision in next cycle if output is not ready."); + + // Trigger this *with* lock_q antecedant to avoid event queue scheduling issues + // over `posedge clk_i`. lock_req : assume property( @(posedge clk_i) disable iff (!rst_ni || flush_i) - lock_d |=> inp_valid_i[idx] == req_q[idx]) + lock_q |-> inp_valid_i[idx] == req_q[idx]) else $fatal(1, "It is disallowed to deassert the selected unserved request signals."); `endif `endif