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}" + )