☣️ [VERDICT]
Prop. 29d found a data/enable/address trio registered together with the address advanced, so word N landed at address N+1 and slot 0 was never written. It was found by accident, in two modules, while investigating something else. The zero-sweep's rule says that after the second sighting of a shape you enumerate the class rather than wait for a third.
The syntactic scan found nothing, which was the wrong question
A regex over every clocked block looking for a self-incremented output co-assigned with an enable returned zero candidates — because both instances had already been fixed. A scan for the broken form of a shape can only find instances nobody has repaired. The useful question is semantic: does every write port present address, data and enable from the same stage?
Three write ports, enumerated
| port |
address source |
enable |
verdict |
wmem weight BRAM |
pf_bram_addr ← word_index |
pf_bram_we |
PROVED contiguous |
amem_a/amem_b activation |
act_wr_word registered index |
act_word_valid |
PROVED contiguous |
| DMA local |
local_addr ← word_index |
local_we |
open — refutes |
The activation port had never been checked at all. It pairs a registered index with a combinational valid — the correct shape — and that is now proved rather than asserted by inspection.
Contiguity is the right property; monotonicity was not
Prop. 29's property required the write address to increase. That permits skipping slot 0 — exactly what the defect did. The stronger property, now guarding all three ports:
always @(posedge clk) if (rst_n && active && we)
a_writes_contiguous: assert (addr == fv_next); // no gap, no repeat, from zero
A property that a known defect would have passed is the wrong property, and the cheapest moment to notice is right after fixing that defect.
Guard checked with the Prop. 12a vacuity oracle — refutes, so it bites. 21 integration properties, all proving.
The DMA port was not re-diagnosed
Its two properties refute. The wrapper's baseline was re-checked with every property neutralised and proves, so the harness is sound and the refutation is real. But the counterexample I extracted showed local_we low throughout, which cannot violate a property guarded on local_we — so the extraction is untrustworthy. Recorded as-is rather than diagnosed with a tool that had just contradicted itself.
30 propositions · 30 gates · 1212 passed, 0 failed · seals 496/496 · engine baseline, module suites, liveness and both size sweeps green.
Three variants for the next wave
A — Fix the counterexample extraction, then close the DMA. Two waves have now stalled on the same open item, and the blocker is no longer the design — it is that I cannot reliably read a trace out of sat -show. Build a small, tested trace reader (verify it on a property with a known counterexample first), then point it at the DMA. Unblocks the only open RTL defect and every future diagnosis.
B — Read-side pairing. Every property so far constrains writes. Reads have the mirror hazard: weight_bram has a one-cycle read latency and Prop. 14 checks the MAC's control alignment, but nothing checks that the activation read address is aligned with the buffer being read, or that a read never precedes the write of the same slot within a layer.
C — Exact-boundary values. Zero and maximum are swept; the boundaries themselves are not. num_words == 4096 exactly, length == 32768 exactly, and single-element transfers where "first" and "last" coincide — historically where terminator logic breaks, and cheap now that the scaled-model technique exists.
☣️ [VERDICT]
Prop. 29d found a data/enable/address trio registered together with the address advanced, so word N landed at address N+1 and slot 0 was never written. It was found by accident, in two modules, while investigating something else. The zero-sweep's rule says that after the second sighting of a shape you enumerate the class rather than wait for a third.
The syntactic scan found nothing, which was the wrong question
A regex over every clocked block looking for a self-incremented output co-assigned with an enable returned zero candidates — because both instances had already been fixed. A scan for the broken form of a shape can only find instances nobody has repaired. The useful question is semantic: does every write port present address, data and enable from the same stage?
Three write ports, enumerated
wmemweight BRAMpf_bram_addr←word_indexpf_bram_weamem_a/amem_bactivationact_wr_wordregistered indexact_word_validlocal_addr←word_indexlocal_weThe activation port had never been checked at all. It pairs a registered index with a combinational valid — the correct shape — and that is now proved rather than asserted by inspection.
Contiguity is the right property; monotonicity was not
Prop. 29's property required the write address to increase. That permits skipping slot 0 — exactly what the defect did. The stronger property, now guarding all three ports:
Guard checked with the Prop. 12a vacuity oracle — refutes, so it bites. 21 integration properties, all proving.
The DMA port was not re-diagnosed
Its two properties refute. The wrapper's baseline was re-checked with every property neutralised and proves, so the harness is sound and the refutation is real. But the counterexample I extracted showed
local_welow throughout, which cannot violate a property guarded onlocal_we— so the extraction is untrustworthy. Recorded as-is rather than diagnosed with a tool that had just contradicted itself.30 propositions · 30 gates · 1212 passed, 0 failed · seals 496/496 · engine baseline, module suites, liveness and both size sweeps green.
Three variants for the next wave
A — Fix the counterexample extraction, then close the DMA. Two waves have now stalled on the same open item, and the blocker is no longer the design — it is that I cannot reliably read a trace out of
sat -show. Build a small, tested trace reader (verify it on a property with a known counterexample first), then point it at the DMA. Unblocks the only open RTL defect and every future diagnosis.B — Read-side pairing. Every property so far constrains writes. Reads have the mirror hazard:
weight_bramhas a one-cycle read latency and Prop. 14 checks the MAC's control alignment, but nothing checks that the activation read address is aligned with the buffer being read, or that a read never precedes the write of the same slot within a layer.C — Exact-boundary values. Zero and maximum are swept; the boundaries themselves are not.
num_words == 4096exactly,length == 32768exactly, and single-element transfers where "first" and "last" coincide — historically where terminator logic breaks, and cheap now that the scaled-model technique exists.