From a58d0b7993dda7b1e9079902c3da25a0bc588ce4 Mon Sep 17 00:00:00 2001 From: Marcos Date: Wed, 6 May 2026 11:18:04 -0300 Subject: [PATCH] feat(rtl): formalize core_mem_rd_data stability contract on global_mem_axi4_adapter MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes #27. PR #25 added test_core1_rd_data_stable_cycle_after_ack in verif/global_mem_controller/, which depends on the implicit invariant that cm_rd_data (driven by global_mem_axi4_adapter.core_mem_rd_data) holds its value until the next request. That invariant was a property of the current single-outstanding implementation, not a written port contract — a future multi-outstanding adapter or response-forwarding optimization could silently glitch the value with no compile-time error and no test failure. This commit elevates the invariant to a public port contract: src/popsolutions/axi4/global_mem_axi4_adapter.sv Adds a 'PUBLIC CONTRACT - core_mem_rd_data stability' header block above the module declaration. States normatively that core_mem_rd_data MUST remain bit-stable from the cycle of core_mem_ack=1 until the cycle BEFORE the next core_mem_rd_req or core_mem_wr_req is sampled high. Documents the remediation path: any future implementation that cannot honor this MUST rename the public port surface so consumers break loudly at integration time rather than silently at runtime. References the enforcing test by full path. verif/global_mem_axi4_adapter/test_global_mem_axi4_adapter.py Adds test_rd_data_stable_between_requests. Pre-loads two distinct values at different cache lines, issues a read at addr A, captures core_mem_rd_data on the ack cycle, then holds the bus idle for 8 clocks while re-sampling every cycle and asserting bit-exact equality with the on-ack value. Also stirs core_mem_addr to 0xDEAD0000 during the idle window to catch any combinational dependency on the address bus, and asserts busy/ack stay deasserted. A final follow-up read of addr B confirms the held value was the genuine prior result, not a stuck driver. Test evidence (verif/global_mem_axi4_adapter): TESTS=7 PASS=7 FAIL=0 SKIP=0 test_reset PASS test_word_roundtrip PASS test_slot_independence_within_line PASS test_all_slots_within_line PASS test_cross_cache_line PASS test_busy_during_transaction PASS test_rd_data_stable_between_requests PASS (new) Regression evidence (verif/global_mem_controller): TESTS=10 PASS=10 FAIL=0 SKIP=0 test_core1_rd_data_stable_cycle_after_ack PASS (PR #25 — still green) Out of scope (separate ADR + PR per issue scope): refactoring the adapter to be multi-outstanding; touching global_mem_controller.sv or other consumers. Authored by Agent 1 (RTL Architect). Signed-off-by: Marcos --- .../axi4/global_mem_axi4_adapter.sv | 57 ++++++++++ .../test_global_mem_axi4_adapter.py | 104 ++++++++++++++++++ 2 files changed, 161 insertions(+) diff --git a/src/popsolutions/axi4/global_mem_axi4_adapter.sv b/src/popsolutions/axi4/global_mem_axi4_adapter.sv index be214f1..a20a2d1 100644 --- a/src/popsolutions/axi4/global_mem_axi4_adapter.sv +++ b/src/popsolutions/axi4/global_mem_axi4_adapter.sv @@ -40,6 +40,63 @@ // * 32-bit aligned core accesses only (lower 2 bits of addr ignored). // * Single outstanding transaction at a time. // * Single-beat AXI4 (AxLEN = 0); bursts are deferred to follow-up issues. +// +// ===================================================================== +// PUBLIC CONTRACT — core_mem_rd_data stability (issue #27) +// ===================================================================== +// +// Stability invariant (NORMATIVE — consumers rely on this): +// +// Once `core_mem_ack` pulses for a read transaction, the value driven on +// `core_mem_rd_data` on that ack cycle MUST remain bit-stable on every +// subsequent clock cycle until — but not including — the cycle on which +// the next `core_mem_rd_req` or `core_mem_wr_req` is sampled high by +// this adapter. +// +// Restated: while the bus is idle (no new req), `core_mem_rd_data` does +// NOT glitch, does NOT change value, and does NOT go to X. The last +// read result is held verbatim. Consumers (e.g. global_mem_controller's +// `core1_*` port group, gpu_die.sv, and any current/future block that +// re-samples the read datum after the ack cycle) MUST be able to rely +// on this for correctness. +// +// Why this contract is written down: +// +// The current implementation satisfies this trivially: it is single- +// outstanding and `core_mem_rd_data` is registered inside +// axi4_master_simple's `req_rdata` and held in place by +// core_axi4_adapter's slot mux until the next request arrives. No +// active read driver chooses to change the value while the bus is +// idle. That is an *implementation* property today, not a +// *port-level* property. +// +// A future multi-outstanding adapter, response-forwarding optimization, +// or a refactor that drives `core_mem_rd_data` directly off `m_rdata` +// (or off any signal that toggles between transactions) could silently +// break this invariant — the affected consumer code (e.g. cm_rd_data +// re-sampling in the controller path that PR #25's regression test +// covers) would then glitch on the cycle after ack with no compile-time +// error and no test failure unless that test is timing-precise. +// +// This block elevates the invariant to a *port contract* of +// global_mem_axi4_adapter. Any future implementation MUST preserve it. +// If a future design genuinely cannot honor it (e.g. true multi- +// outstanding with out-of-order response forwarding), the public port +// surface MUST be renamed (e.g. `core_mem_rd_data_valid` + a separate +// capture register exposed to the consumer) so existing consumers +// break loudly at integration time rather than silently at runtime. +// +// Test that enforces this contract: +// +// verif/global_mem_axi4_adapter/test_global_mem_axi4_adapter.py :: +// test_rd_data_stable_between_requests +// +// The test issues a read, captures `core_mem_rd_data` on the ack +// cycle, then holds the bus idle for >=8 clocks while re-sampling +// `core_mem_rd_data` on every cycle. Every sample must equal the +// on-ack value. +// +// ===================================================================== `default_nettype none diff --git a/verif/global_mem_axi4_adapter/test_global_mem_axi4_adapter.py b/verif/global_mem_axi4_adapter/test_global_mem_axi4_adapter.py index eb8fd65..054e307 100644 --- a/verif/global_mem_axi4_adapter/test_global_mem_axi4_adapter.py +++ b/verif/global_mem_axi4_adapter/test_global_mem_axi4_adapter.py @@ -173,3 +173,107 @@ async def test_busy_during_transaction(dut): assert saw_busy, "core_mem_busy never asserted during the transaction" await RisingEdge(dut.clk) assert dut.core_mem_busy.value == 0 + + +@cocotb.test() +async def test_rd_data_stable_between_requests(dut): + """Enforces the public stability contract on `core_mem_rd_data`. + + Issue #27 / PR #25 follow-up: consumers (e.g. global_mem_controller's + `core1_*` port group, gpu_die.sv) re-sample `core_mem_rd_data` on + cycles AFTER the ack cycle. The adapter is therefore required to + hold the read datum bit-stable from the ack cycle through every + idle cycle until — but not including — the cycle on which the next + `core_mem_rd_req` or `core_mem_wr_req` is sampled high. + + Procedure: + 1. Pre-load known data at addr A via a write. + 2. Pre-load DIFFERENT known data at addr B (a separate cache line) + so the underlying memory backing definitely toggles between + the two values — this means a future broken implementation + that, say, drove `core_mem_rd_data` off `m_rdata` (which IS + allowed to glitch when the AXI4 bus does other work) would be + caught. + 3. Issue a read at addr A; capture the value on the ack cycle. + 4. Hold the bus idle (rd_req = wr_req = 0) for IDLE_HOLD_CYCLES + cycles, sampling `core_mem_rd_data` every cycle. Each sample + MUST equal the captured on-ack value, bit-exact. + + Failing this test indicates an implementation-level optimization + has silently broken the port-level invariant documented in + src/popsolutions/axi4/global_mem_axi4_adapter.sv. See that file's + 'PUBLIC CONTRACT - core_mem_rd_data stability' header block for the + full normative statement and remediation guidance. + """ + cocotb.start_soon(Clock(dut.clk, CLK_PERIOD_NS, unit="ns").start()) + await reset_dut(dut) + + addr_a = 0x100 + addr_b = 0x140 # different cache line (32-byte stride) + word_a = 0xA5A5A5A5 + word_b = 0x5A5A5A5A + + # Pre-load both addresses so memory holds distinct, distinguishable + # values. This makes a hypothetical broken implementation that + # forwarded m_rdata directly visible — m_rdata would necessarily + # change between transactions, so any leakage onto core_mem_rd_data + # during the idle window would show up. + await core_write(dut, addr_a, word_a) + await core_write(dut, addr_b, word_b) + + # Issue a read of addr_a; capture the on-ack datum manually so we + # see the EXACT cycle the contract starts on. + dut.core_mem_addr.value = addr_a + dut.core_mem_rd_req.value = 1 + await RisingEdge(dut.clk) + dut.core_mem_rd_req.value = 0 + + on_ack_value = None + for _ in range(300): + await RisingEdge(dut.clk) + if dut.core_mem_ack.value == 1: + on_ack_value = int(dut.core_mem_rd_data.value) + break + assert on_ack_value is not None, "read of addr_a never acked" + assert on_ack_value == word_a, ( + f"sanity: on-ack rd_data mismatch: expected 0x{word_a:08x}, " + f"got 0x{on_ack_value:08x}" + ) + + # Now the contract window. Hold the bus idle and re-sample every + # cycle. Each sample must equal on_ack_value. + IDLE_HOLD_CYCLES = 8 + dut.core_mem_rd_req.value = 0 + dut.core_mem_wr_req.value = 0 + # Stir the address bus to make sure rd_data isn't accidentally + # combinational on `core_mem_addr` — that would also be a contract + # violation (consumers may park any address there while idle). + dut.core_mem_addr.value = 0xDEAD0000 + + for cycle in range(IDLE_HOLD_CYCLES): + await RisingEdge(dut.clk) + sample = int(dut.core_mem_rd_data.value) + assert sample == on_ack_value, ( + f"core_mem_rd_data GLITCHED on idle cycle +{cycle + 1} after ack: " + f"on-ack value was 0x{on_ack_value:08x}, " + f"now reads 0x{sample:08x}. " + f"This violates the stability contract documented in " + f"src/popsolutions/axi4/global_mem_axi4_adapter.sv " + f"('PUBLIC CONTRACT - core_mem_rd_data stability')." + ) + # Also: busy/ack must stay deasserted during the idle window. + assert dut.core_mem_busy.value == 0, ( + f"core_mem_busy unexpectedly asserted on idle cycle +{cycle + 1}" + ) + assert dut.core_mem_ack.value == 0, ( + f"core_mem_ack unexpectedly asserted on idle cycle +{cycle + 1} " + f"(no new request was issued)" + ) + + # Final cross-check: a follow-up read of addr_b returns word_b. + # Confirms the adapter is still functional and the held value was + # genuinely the prior result, not a stuck driver. + got_b = await core_read(dut, addr_b) + assert got_b == word_b, ( + f"follow-up read mismatch: expected 0x{word_b:08x}, got 0x{got_b:08x}" + )