fix(bitnet): pair the DMA local write address with its own beat (Closes #2003)

[gHashTag]

Closes #2003

The defect is live on master verbatim

#2003 reports itself as fixed. Its fixes landed on a branch that never merged (no PR, in any state), so the defect is live. Confirmed against freshly-fetched origin/master (cb1f0d4eb9805d7e3b947b13cb53b299d50c969c) — bootstrap/src/bitnet_dma.rs:195-196:

    s.push_str("                local_we        <= 1'b1;\n");
    s.push_str("                local_addr      <= local_addr + 12'd1;\n");

Both are non-blocking, so both land on the same edge: the cycle the strobe goes high, the address has already advanced. Beat 0 is captured while local_addr is 0, but the memory sees we=1 with addr=1. Every beat is written one slot high and address 0 is never written at all.

The change

Add a beat_index counter. READ_DATA drives local_addr <= beat_index; and advances beat_index <= beat_index + 12'd1;, so address, data and enable are all registered from the same stage and describe the same beat. beat_index is cleared at reset and re-armed in the IDLE start branch.

WRITE_DATA is deliberately untouched — there local_addr is a read pointer and its post-increment is correct.

Differential simulation — old and new emitter in one testbench

4-beat read, identical well-behaved AXI slave driving both DUTs:

--- OLD emitter (origin/master) ---        --- NEW emitter (fixed) ---
  local writes = 4                          local writes = 4
    write[0] addr=1 data=d0d0000000000000     write[0] addr=0 data=d0d0000000000000
    write[1] addr=2 data=d0d0000000000001     write[1] addr=1 data=d0d0000000000001
    write[2] addr=3 data=d0d0000000000002     write[2] addr=2 data=d0d0000000000002
    write[3] addr=4 data=d0d0000000000003     write[3] addr=3 data=d0d0000000000003
  mem[0] = ffffffffffffffff                 mem[0] = d0d0000000000000
=== CONTROL: WRITE transfer (direction=1), unchanged path ===
  old AXI w-beats = 3   new AXI w-beats = 3
RESULT: PASS

Slot 0 goes from never-written to correctly written; the control (AXI write-channel beat count on the untouched direction=1 path) is unchanged in both.

Mutant evidence

Guard 1 — read_data_pairs_address_with_data_and_enable. Mutant: revert the READ_DATA arm to master's shape. Fails with:

READ_DATA must not post-increment `local_addr` in the same non-blocking group that raises
`local_we`: the increment lands in the same cycle as the strobe, so beat 0's data is
written to address 1 and slot 0 is never written. READ_DATA arm was:
READ_DATA: if (m_axi_rvalid) begin
                local_wdata     <= m_axi_rdata;
                local_we        <= 1'b1;
                local_addr      <= local_addr + 12'd1;
                bytes_remaining <= bytes_remaining - 32'd8;
                if (m_axi_rlast || bytes_remaining <= 32'd8) state <= DONE_ST;
            end else local_we <= 1'b0;
test result: FAILED. 18 passed; 1 failed

The message prints the offending arm — that is what shows the assertion read the right text.

Here an unanchored guard would have been WRONG, not merely vacuous — measured. WRITE_DATA legitimately keeps its own local_addr <= local_addr + 12'd1;. A naive !v.contains("local_addr + 12'd1") therefore fails on the CORRECT emitter:

test tests::unanchored_guard_ON_THE_CORRECT_EMITTER ... FAILED
unanchored: WRITE_DATA legitimately keeps its own increment

The guard slices the READ_DATA arm out first, so it can be satisfied — or broken — only by the state it is about.

Guard 2 — beat_index_rearmed_in_idle_not_only_at_reset, planted separately. One mutant per guard, not one per file. Mutant: delete only the IDLE re-arm. Fails with:

`beat_index` must be cleared in the IDLE start branch alongside `local_addr`, not only in
the reset block: without it the second transfer after power-on starts writing at a stale
index. IDLE arm was:
IDLE: if (start) begin
                busy            <= 1'b1;
                ...
                local_addr      <= 12'd0;

Guard 1 still passes under this mutant, so neither guard masks the other. Note the reset block still contains beat_index <= 12'd0; under this mutant — so the guard is provably not satisfied by the reset line, which is the trap that had to be repaired hours after landing elsewhere in this campaign.

Reverting every mutant: 19 passed, 0 failed. The emitted Verilog parses under iverilog -g2005.

Pre-existing gap, recorded not papered over

These tests are not executed by CI. No workflow runs cargo test -p t27c; corpus-ratchet.yml records that the step was removed by #2292 after going red on master. Run with rustc --test on the module, which is self-contained.

Adjacent problems seen and deliberately NOT fixed here

• Wave Loop 557 — dma_controller abandoned bursts and advanced on ready-without-valid #1970 — arlen/awlen still hardwired to 8'hFF; READ_ADDR still advances on if (m_axi_arready) with no arvalid; READ_DATA still exits on m_axi_rlast || bytes_remaining <= 32'd8. Deriving the burst length requires a multi-burst FSM (the local memory is 12-bit addressed = 4096 beats, i.e. up to 16 maximal bursts), which is a redesign, not this diff.
• The module has no wstrb, so a length that is not a multiple of 8 over-reads to the next 8-byte boundary.
• DONE_ST is entered without ever waiting on m_axi_bvalid on the write path (assign m_axi_bready = 1'b1; and bvalid is never sampled), so done can rise before the slave has accepted the write response.

Not fixed here, and not filed as fixed. Nothing was weakened: no || true, no continue-on-error, no existing assertion relaxed, no case dropped.

[github-actions]

📓 NotebookLM Notebook linked to this PR

• Notebook ID: b83263109fb055dc
• URL: https://notebooklm.google.com/notebook/b83263109fb055dc

This notebook contains session context, decisions, and artifacts for this work.

[github-actions]

PR Dashboard

Generated at: 2026-08-21 16:13:31 UTC

• fix(bitnet): pair the DMA local write address with its own beat (Closes #2003) #2345 fix(bitnet): pair the DMA local write address with its own beat (Closes #2003) | Created: 2026-08-21 | Updated: 2026-08-21 | 13 failing / 25 total
• fix(bitnet): make the DMA local write strobe a pulse, not a level #2339 fix(bitnet): make the DMA local write strobe a pulse, not a level | Created: 2026-08-21 | Updated: 2026-08-21 | 4 failing / 34 total
• corpus: freeze the damage, patch one class at a time, and say where one rule stops #2161 corpus: freeze the damage, patch one class at a time, and say where one rule stops | Created: 2026-08-14 | Updated: 2026-08-21 | 0 failing / 9 total
• Unbreak FPGA CI and correct two unbacked hardware claims #2081 Unbreak FPGA CI and correct two unbacked hardware claims | Created: 2026-08-11 | Updated: 2026-08-20 | 5 failing / 27 total

Summary

Status	Count
Total Open PRs	4
PRs with Failing Checks	2
PRs with All Checks Green	2
READY	1
FAILING	2
PENDING	0

Seal Status

• ⚠️ STALE -- sha256(compiler.rs)=65f033d04125 != manifest seal=87e5cbd3ad94.
  The committed NMSE numbers were certified against an older compiler.rs.
  Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).