☣️ [VERDICT]
Wave 575 swept the zero end of every count and found two real defects. This is the maximum end, never examined. The shape: a count wider than the thing it indexes.
| module |
count |
address it drives |
ratio |
weight_prefetch_ctrl |
num_words 16 bits |
bram_addr 12 bits |
16× |
dma_controller |
length 32 bits |
local_addr 12 bits |
128× |
The first verdict was a bound artifact, and looked like good news
The monotonicity property proved at -seq 24 on both modules. True, and worthless: reaching address 4096 takes 4096 writes, so the counterexample is unreachable by construction. It proves "no wrap within 24 cycles", which nobody doubted.
Before believing a bounded proof, ask how many cycles a violation would need. If the answer exceeds the bound, the verdict is structural, not empirical.
Scaling the address to 3 bits — the same trick as chparam -set DEPTH 4 weight_bram — brought the wrap inside the bound. Both refuted immediately.
Defect 1 — the address wraps and overwrites
Past 4096 entries the counter wraps to zero and the transfer keeps writing over data it already fetched, then reports success. Silent corruption. Both modules now clamp to the address space and raise a new overflow output.
The error IRQ existed and was tied off
bitnet_engine_top had .error(1'b0) — a sticky, maskable, read-to-clear status bit nothing could ever set. An oversized request is exactly what it is for. Both overflow outputs now drive it: the request completes, nothing is corrupted, and the host is told.
Defect 2 — every word was written one slot too high
Found only because defect 1's fix did not make the property pass. Data, write-enable and address increment are non-blocking assignments in the same cycle, so the memory sees the post-increment address:
bram_data <= axi_rdata[53:0];
bram_we <= 1'b1;
bram_addr <= bram_addr + 12'd1; // word N lands at address N+1
Address 0 was never written in either transfer engine, and the final word wrapped over it. Both now write at the word's own index. This had nothing to do with sizing — it surfaced because a property that should have passed after a correct fix didn't, and the gap was investigated instead of papered over.
Prefetch proved, DMA open
The scaled prefetch proves, and refutes again with the clamp removed — discriminating both ways. The DMA, with identical fixes applied, still refutes, and the cause is not identified. Two patches tried; neither closed it. Gated as an expected refutation rather than guessed at a third time.
Two environment faults were mine: comparing write addresses across two different transfers, and leaving m_axi_rlast free so the solver played a slave that never ends a burst. An unconstrained input is an adversary — a refutation is a claim about the environment until the environment is pinned down.
29 propositions · 29 gates · 1211 passed, 0 failed · seals 496/496 · module suites, engine baseline, 20 integration properties, liveness and the zero-size sweep all still green. Details: docs/FORMAL_FOUNDATIONS.md Prop. 29.
Three variants for the next wave
A — Close the DMA address property. The one thing this wave started and did not finish. Same two fixes as the prefetch are in place, yet it refutes; the honest next step is a counterexample trace read carefully rather than a third patch. Highest-value because it is a known-unknown in code that already carries two confirmed defects.
B — Sweep the remaining boundary classes. Zero and maximum are done for counts. Untouched: off-by-one at both ends (num_words == 4096 exactly, length == 32768 exactly), and single-element transfers, where the "last" and "first" conditions coincide — historically where terminator logic breaks.
C — Audit every registered-output pairing in the bundle. Defect 2 was a data/address/enable trio registered together where one member was advanced. That is a shape, and this wave found it in two modules by accident. Enumerate every output reg written alongside a counter increment and check each pairing. The zero-sweep found two instances of one shape in one pass; this would do the same for a shape that silently corrupts data.
☣️ [VERDICT]
Wave 575 swept the zero end of every count and found two real defects. This is the maximum end, never examined. The shape: a count wider than the thing it indexes.
weight_prefetch_ctrlnum_words16 bitsbram_addr12 bitsdma_controllerlength32 bitslocal_addr12 bitsThe first verdict was a bound artifact, and looked like good news
The monotonicity property proved at
-seq 24on both modules. True, and worthless: reaching address 4096 takes 4096 writes, so the counterexample is unreachable by construction. It proves "no wrap within 24 cycles", which nobody doubted.Scaling the address to 3 bits — the same trick as
chparam -set DEPTH 4 weight_bram— brought the wrap inside the bound. Both refuted immediately.Defect 1 — the address wraps and overwrites
Past 4096 entries the counter wraps to zero and the transfer keeps writing over data it already fetched, then reports success. Silent corruption. Both modules now clamp to the address space and raise a new
overflowoutput.The error IRQ existed and was tied off
bitnet_engine_tophad.error(1'b0)— a sticky, maskable, read-to-clear status bit nothing could ever set. An oversized request is exactly what it is for. Bothoverflowoutputs now drive it: the request completes, nothing is corrupted, and the host is told.Defect 2 — every word was written one slot too high
Found only because defect 1's fix did not make the property pass. Data, write-enable and address increment are non-blocking assignments in the same cycle, so the memory sees the post-increment address:
Address 0 was never written in either transfer engine, and the final word wrapped over it. Both now write at the word's own index. This had nothing to do with sizing — it surfaced because a property that should have passed after a correct fix didn't, and the gap was investigated instead of papered over.
Prefetch proved, DMA open
The scaled prefetch proves, and refutes again with the clamp removed — discriminating both ways. The DMA, with identical fixes applied, still refutes, and the cause is not identified. Two patches tried; neither closed it. Gated as an expected refutation rather than guessed at a third time.
Two environment faults were mine: comparing write addresses across two different transfers, and leaving
m_axi_rlastfree so the solver played a slave that never ends a burst. An unconstrained input is an adversary — a refutation is a claim about the environment until the environment is pinned down.29 propositions · 29 gates · 1211 passed, 0 failed · seals 496/496 · module suites, engine baseline, 20 integration properties, liveness and the zero-size sweep all still green. Details:
docs/FORMAL_FOUNDATIONS.mdProp. 29.Three variants for the next wave
A — Close the DMA address property. The one thing this wave started and did not finish. Same two fixes as the prefetch are in place, yet it refutes; the honest next step is a counterexample trace read carefully rather than a third patch. Highest-value because it is a known-unknown in code that already carries two confirmed defects.
B — Sweep the remaining boundary classes. Zero and maximum are done for counts. Untouched: off-by-one at both ends (
num_words == 4096exactly,length == 32768exactly), and single-element transfers, where the "last" and "first" conditions coincide — historically where terminator logic breaks.C — Audit every registered-output pairing in the bundle. Defect 2 was a data/address/enable trio registered together where one member was advanced. That is a shape, and this wave found it in two modules by accident. Enumerate every
output regwritten alongside a counter increment and check each pairing. The zero-sweep found two instances of one shape in one pass; this would do the same for a shape that silently corrupts data.