chore(rtl): re-apply dead contr_rd_addr_q removal lost in PR #19 squash#26
Merged
marcos-mendez merged 1 commit intomainfrom May 6, 2026
Merged
Conversation
This was referenced May 6, 2026
marcos-mendez
added a commit
that referenced
this pull request
May 6, 2026
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 <popsolutions.co@gmail.com>
Co-authored-by: Marcos <popsolutions.co@gmail.com>
7 tasks
marcos-mendez
added a commit
that referenced
this pull request
May 6, 2026
…tation (#40) Adds `test_back_to_back_contr_rd_drops_second` to verif/global_mem_controller/test_global_mem_controller.py — the CANARY demanded by MAST issue #21. The arbiter in src/global_mem_controller.sv defers a contr_rd_en pulse that arrives during a busy cycle into a single-deep `contr_rd_pending` latch. Today's caller (gpu_controller.sv) holds each request pending its own ack handshake, so depth-1 is sufficient AT THIS MOMENT. When gpu_controller.sv migrates to AXI4 (Phase 3 of the parameter-taxonomy plan), or any future caller can issue back-to-back contr_rd_en pulses, this assumption breaks: a second pulse arriving while pending is set will silently overwrite the first. The new test pins this behaviour: * Pre-loads distinct sentinels at addr_a / addr_b / addr_c * Holds the AXI4 adapter busy with a core1 read at addr_c * Pulses contr_rd_en for addr_a then addr_b on consecutive cycles * Asserts BOTH acks land — the post-fix behaviour * `@cocotb.test(expect_fail=True)` flips the assertion failure into a regression PASS today, so the suite stays green while the gap is documented in-place The test fires the assertion exactly as predicted (saw 1 ack carrying word_b=0xBBBBBBBB; word_a=0xAAAAAAAA was lost), proving the depth-1 gap empirically. After a future fix widens the latch to a FIFO (depth N>=2) or adds a contr_rd_busy back-pressure output, the test will start passing functionally — at which point the expect_fail=True marker must be removed (instructions are in the test docstring). Out of scope per issue #21: widening the latch, redesigning the arbiter, ADR work. This PR is canary-only. Refs: MAST #21, MAST #19 (the merged arbiter), MAST #24/#26 (the SVA invariant that already guards the inflight/pending mutual exclusion). TESTS=11 PASS=11 FAIL=0 SKIP=0 Authored by Agent 1 (RTL Architect). Signed-off-by: Marcos <m@pop.coop> Co-authored-by: Marcos <m@pop.coop>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Context
PR #19 (merged 2026-05-06 as
2eb0724) was reviewed by Agent R and one finding was self-fixed by Agent R via commitd2aaef3(3-line removal of deadcontr_rd_addr_qregister). CI ran green ond2aaef3before merge. After the squash merge, however, the resulting commit on main (2eb0724) contained only the original PR head's content — the fix commitd2aaef3was not included.Hypothesis: GitHub squash merge pulls the PR head SHA via API at the moment of
merge_pull_request; if the local push of the fix commit hadn't yet propagated to the PR'shead_reffield at that exact moment (race betweengit pushand PR head_ref update), the squash captures the stale state. CI still ran on the latest commit (which is why it appeared green) but the merge captured the prior state.Filing this fix-up PR via the GitHub Contents API to avoid local working-tree collision with concurrently-running Agent 1 round 2 (which already branched from
2eb0724).Fix
Removes 3 lines from
src/global_mem_controller.sv:reg [addr_width-1:0] contr_rd_addr_q;)contr_rd_addr_q <= '0;)contr_rd_addr_q <= contr_rd_req_addr;)The register is declared, reset, and written but never read — confirmed dead state. Removing saves a 32-bit flop per instance and clarifies the FSM intent.
Test evidence
This fix was already validated in PR #19's review cycle:
TESTS=7 PASS=7 FAIL=0 SKIP=0after the same removal was applied locally. CI re-runs on this PR will confirm.Process improvement (logged in working-dir
task-to-marcos.mditem #5)Updating Agent R protocol: after
git pushto a PR branch, verifygh pr view N --json headRefOidmatches the local SHA before callinggh pr merge. Marcos to decide whether to formalize as a hook or keep as a manual convention.Authored by Agent R (Reviewer).