From ccde07db31dbf0ebea0ce9a9d9d32c3fafcf6afd Mon Sep 17 00:00:00 2001 From: Marcos Date: Wed, 6 May 2026 12:02:36 -0300 Subject: [PATCH] feat(rtl): SVA assert for contr_rd arbiter invariant (closes #24) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add a SystemVerilog concurrent assertion making the `!(contr_rd_inflight && contr_rd_pending)` invariant explicit and machine-checkable in simulation. The state machine in global_mem_controller already guarantees this invariant: when `grant_contr_rd` fires, `contr_rd_inflight` is set AND `contr_rd_pending` is cleared in the same cycle. Both being high simultaneously means a contr_rd is mid-AXI4-transaction AND another is queued behind it — a state the response demultiplexer is not designed to handle, and a sign that a future refactor has broken the grant logic. The assertion uses the standard `assert property` SVA form. Verilator 5.x accepts concurrent assertions by default (assertions enabled unless `--no-assert` is passed), so no Makefile change is required. The whole block is wrapped in `\`ifndef SYNTHESIS` so synthesis tools that don't grok SVA skip it cleanly. Verification: a temp testbench (not committed) deposited `contr_rd_inflight=1; contr_rd_pending=1` simultaneously and the assertion fired as expected: [70000] %Error: global_mem_controller.sv:242: Assertion failed in global_mem_controller: [70000] global_mem_controller: arbiter invariant violated — contr_rd_inflight && contr_rd_pending both high All 10 existing cocotb tests in verif/global_mem_controller still pass (test counts before/after: 10/10 → 10/10). Refs: MAST issue #24, PR #19 (arbiter introduction), PR #26 (dead-reg fix). Authored by Agent 1 (RTL Architect). Signed-off-by: Marcos --- src/global_mem_controller.sv | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/global_mem_controller.sv b/src/global_mem_controller.sv index 6391bd8..2520aab 100644 --- a/src/global_mem_controller.sv +++ b/src/global_mem_controller.sv @@ -220,6 +220,29 @@ module global_mem_controller ( end end + // =================================================================== + // Arbiter invariant (MAST issue #24). + // + // `contr_rd_inflight` and `contr_rd_pending` MUST never be high in + // the same cycle. The state machine above guarantees this by clearing + // `contr_rd_pending` in the same cycle `grant_contr_rd` sets + // `contr_rd_inflight`. Both being high simultaneously would mean a + // contr_rd is mid-AXI4-transaction AND another is queued behind it — + // a state the response demultiplexer is not designed to handle, and + // a sign that a future refactor has broken the grant logic (e.g. + // someone changed the grant condition without clearing pending). + // + // Wrapped in `ifndef SYNTHESIS` so synthesis tools that don't grok + // SystemVerilog concurrent assertions skip it cleanly. Verilator 5.x + // accepts `assert property` by default (assertions are on unless + // `--no-assert` is passed), so no Makefile change is required. + `ifndef SYNTHESIS + assert property (@(posedge clk) disable iff (!rst) + !(contr_rd_inflight && contr_rd_pending)) + else $error("[%0t] global_mem_controller: arbiter invariant violated — contr_rd_inflight && contr_rd_pending both high", + $time); + `endif + // =================================================================== // Response demultiplex: ack / rd_data are routed to whichever // requester is currently tracked. core1_busy stays asserted whenever