From dd0bd39cad4807552e6bb8c8fe976bfc9965be0f Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sat, 22 Aug 2026 14:46:50 +0700 Subject: [PATCH] test(bitnet): assert the DMA address advance per state arm, not by literal count dma_local_addr_autoincrement_both_paths counted one literal across the whole module and required two. #2345 replaced the read path's post-increment with local_addr <= beat_index -- the #2003 fix -- so the count fell to one and the test has been red on master since. The emitter is correct; the test was stale. A global count cannot say which path a match came from, which is what let the read path lose its advance while the assertion still saw one match. Lowering the threshold to >= 1 would go green and re-open the same blind spot. Now sliced per state arm. Invisible until now because cargo test stops at the first failing target and this is the 42nd of 73 (#2382). Closes #2384 --- bootstrap/tests/bitnet_dma.rs | 58 ++++++++++++++++++++++--- docs/now/2026-08-22-dma-addr-per-arm.md | 45 +++++++++++++++++++ scripts/ci/test-baseline.txt | 3 +- 3 files changed, 99 insertions(+), 7 deletions(-) create mode 100644 docs/now/2026-08-22-dma-addr-per-arm.md diff --git a/bootstrap/tests/bitnet_dma.rs b/bootstrap/tests/bitnet_dma.rs index f8af8a8923..5e806fc982 100644 --- a/bootstrap/tests/bitnet_dma.rs +++ b/bootstrap/tests/bitnet_dma.rs @@ -203,18 +203,66 @@ fn dma_rlast_or_count_terminates_read() { .contains("if (m_axi_rlast || bytes_remaining <= 32'd8) state <= DONE_ST;")); } +/// Both transfer paths must advance the local address, but they do it by +/// different mechanisms and a single literal cannot see both. +/// +/// This test used to count occurrences of `local_addr <= local_addr + 12'd1;` +/// across the whole module and require two. #2345 replaced the read path's +/// post-increment with `local_addr <= beat_index` — deliberately, because the +/// post-increment landed beat 0's data at address 1 and never wrote slot 0 — +/// so the count fell to one and the test failed. The test was stale, not the +/// emitter: the *property* it meant to hold (each path advances the +/// destination address) is still true. +/// +/// It went unnoticed because `cargo test -p t27c --tests` stops at the first +/// failing target and this one is 42nd, so it never ran. See #2382. +/// +/// Anchored per state arm rather than counted globally: a count over the whole +/// output cannot tell which path a match came from, which is what let the read +/// path silently lose its advance. #[test] -fn dma_local_addr_autoincrement_both_paths() { +fn dma_local_addr_advances_on_both_paths() { let (stdout, _stderr, ok) = run(&["gen-dma-controller"]); assert!(ok); - let bumps = stdout.matches("local_addr <= local_addr + 12'd1;").count(); + + let read_arm = arm(&stdout, "READ_DATA: if (m_axi_rvalid) begin", "end else local_we"); + // The read path presents the beat's own index, so beat 0 lands at address 0. + assert!( + read_arm.contains("local_addr <= beat_index;"), + "READ_DATA must present the beat index as the address, not post-increment \ + (that was #2003 — beat 0 landed at address 1 and slot 0 was never written). \ + READ_DATA arm was:\n{}", + read_arm + ); + assert!( + read_arm.contains("beat_index <= beat_index + 12'd1;"), + "READ_DATA must advance beat_index, or every beat writes address 0. \ + READ_DATA arm was:\n{}", + read_arm + ); + + // The write path's local_addr is a read pointer into local memory, so a + // post-increment is correct there and must not be "fixed" to match the read path. + let write_arm = arm(&stdout, "WRITE_DATA: begin", "WRITE_RESP"); assert!( - bumps >= 2, - "expected local_addr++ on both read and write beats, got {}", - bumps + write_arm.contains("local_addr <= local_addr + 12'd1;"), + "WRITE_DATA must advance local_addr, or every beat reads the same word. \ + WRITE_DATA arm was:\n{}", + write_arm ); } +/// Slice from `start` to the next `end_marker`, so an assertion cannot be +/// satisfied by an identical line in a different state. +fn arm<'a>(hay: &'a str, start: &str, end_marker: &str) -> &'a str { + let from = hay + .find(start) + .unwrap_or_else(|| panic!("state arm not found: {start}\nin:\n{hay}")); + let rest = &hay[from..]; + let to = rest.find(end_marker).unwrap_or(rest.len()); + &rest[..to] +} + // ============================================================================ // Reset & DONE handling // ============================================================================ diff --git a/docs/now/2026-08-22-dma-addr-per-arm.md b/docs/now/2026-08-22-dma-addr-per-arm.md new file mode 100644 index 0000000000..5d4b8dea4c --- /dev/null +++ b/docs/now/2026-08-22-dma-addr-per-arm.md @@ -0,0 +1,45 @@ +# NOW — a stale test counted a literal the emitter stopped writing + +Last updated: 2026-08-22 + +## Assert the address advance per state arm (Closes #2384) + +- Branch: `fix/2384-dma-addr-per-arm` +- Issue: #2384 + +### Что легло + +`bootstrap/tests/bitnet_dma.rs` — `dma_local_addr_autoincrement_both_paths` becomes +`dma_local_addr_advances_on_both_paths`, asserting each path's mechanism inside its own +state arm instead of counting one literal across the module. Plus one line pruned from +`scripts/ci/test-baseline.txt` (383 → 382), since the test now passes. + +The test had been red on master since #2345, which replaced the read path's post-increment +with `local_addr <= beat_index` — correctly, that was the #2003 fix — and did not update +the test that counted the old literal. **The emitter is right; the test was stale.** + +The property is unchanged and still holds: each path advances the destination address. +`READ_DATA` presents `beat_index` and advances it; `WRITE_DATA` post-increments +`local_addr`, which is a read pointer there and must not be harmonised with the read path. + +### Границы честности (BINDING) + +- **Not a fix to any emitted RTL.** No Verilog changes. This corrects a test that was + measuring surface form instead of the property it names. +- Lowering the threshold from `>= 2` to `>= 1` would also have gone green and would have + re-opened the same blind spot — a global count cannot say which path a match came from. +- The failure was invisible because `cargo test` stops at the first failing target and this + is the 42nd of 73 (#2382). The ratchet landed in #2383 is what will surface the next one. +- **This is one of the 12 unexamined failures from #2382. Eleven remain**, and their ages + are still unestablished. + +### Evidence + +Three mutants, one per assertion, each verified planted (`planted=1`) before the run and +each caught by exactly its own assertion: + +- `bitnet_dma.rs:217` removed → `READ_DATA must present the beat index as the address…` +- `:218` removed → `READ_DATA must advance beat_index, or every beat writes address 0.` +- `:235` removed → `WRITE_DATA must advance local_addr, or every beat reads the same word.` + +`21 passed; 1 failed` each time; restored, `22 passed; 0 failed`. diff --git a/scripts/ci/test-baseline.txt b/scripts/ci/test-baseline.txt index 85171498a2..871a25f8ba 100644 --- a/scripts/ci/test-baseline.txt +++ b/scripts/ci/test-baseline.txt @@ -1,7 +1,7 @@ # Generated by scripts/ci/test_ratchet.py --emit-baseline. # Do not hand-edit: regenerate from a real --no-fail-fast log. # Each line is targettest for a test failing on master. -# 73 targets ran; 383 failing tests. +# 73 targets ran; 382 failing tests (one pruned by #2384). src/main.rs compiler::tests_compiler_rejects::lowers_only_first_of_two_modules_characterization src/main.rs compiler::tests_phase40_coverage::test_for_range_loop_unroll src/main.rs compiler::tests_phase40_coverage::test_parse_for_range @@ -15,7 +15,6 @@ src/main.rs compiler::tests_w458::tests_w459::array_param_bound_from_test_block src/main.rs compiler::tests_w458::tests_w459::test_block_emits_real_function_call src/main.rs lex_conform::tests::lexer_matches_its_conformance_table src/main.rs parse_conform::tests::parser_matches_its_conformance_table -tests/bitnet_dma.rs dma_local_addr_autoincrement_both_paths tests/bitnet_layer.rs spec_first_layer2_packs_two_neuron_trits tests/bitnet_mlp.rs spec_first_mlp2_two_layer_inference_matches_reference tests/bitnet_mlp3.rs spec_first_mlp3_three_layer_inference_matches_reference