☣️ [VERDICT]
Two waves stalled on one open finding, and the blocker had stopped being the design. Prop. 30e recorded a counterexample in which the guard signal was low throughout — which cannot violate a property guarded on that signal — and correctly refused to reason from it. This wave fixed the instrument.
yosys sat -dump_json emits invalid JSON
{ "name": "$auto$async2sync.cc:107:execute$243", "wave": "0.1..." }
^ \e is not a JSON escape
RTLIL names are written verbatim, backslashes and all. formal/trace_reader.py repairs stray backslashes before parsing, and expands WaveJSON properly — . repeats the previous value, = consumes the next data entry. A reader that ignores . loses most of the trace: the same failure one layer down.
Validated before use
The reader is pointed at a property whose counterexample is known — the prefetch with its clamp removed, which must show a write at a wrapped address. It parses 91 signals and finds the wrap at t=18. That check is a CI step.
Verify the instrument on a case whose answer you already know, before trusting it on one you don't. The reader that produced two waves of confusion would have failed this check in one second.
With it working, the defect was legible immediately
The first query — not eyeballing, but asking at which timestep does the guard hold and the assertion fail — returned t=28: local_addr=1, expected 0. The first write of a transfer was landing at address 1. Two mechanisms, both fixed:
local_addr served two roles — write pointer when data comes from the bus, read pointer when it goes to it. Prop. 29d gave only one role its own index, so the two fought. Both paths now share one sequential index.- The pointer reset sat inside the
length != 0 branch. A zero-length request takes the DONE path and left the pointers where the previous transfer put them. Reset now happens on every start.
Still open, for a stated reason
After both fixes the property still refutes. That is the third patch; the rule from Prop. 29 — after two failed attempts, read the counterexample rather than patch again — was followed, produced two real defects, and did not exhaust the cause. It stays gated as an expected refutation. What changed is that the next investigation starts with a working instrument.
Both fixes were kept. Neither closed the target property, which by Prop. 25's standard is grounds for withdrawal. They were kept because each is independently correct and nothing regressed — module suites, engine baseline, 21 integration properties and the full zero-size sweep all pass.
31 propositions · 31 gates · 1212 passed, 0 failed · seals 496/496.
Three variants for the next wave
A — Finish the DMA with the working instrument. The next query is cheap now: dump the trace after the two fixes and find the third mechanism. Three waves of accumulated context plus a validated reader is the best position this item has ever been in.
B — Read-side pairing. Every property so far constrains writes. Nothing checks that an 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 — the mirror of the defect class that has produced four findings.
C — Point the reader at every existing refutation. Two open properties are gated as expected refutations, and each was diagnosed with the broken instrument or not at all. Re-read both traces now that the reader works; a gated refutation whose cause was never actually read is a finding waiting to be misfiled.
☣️ [VERDICT]
Two waves stalled on one open finding, and the blocker had stopped being the design. Prop. 30e recorded a counterexample in which the guard signal was low throughout — which cannot violate a property guarded on that signal — and correctly refused to reason from it. This wave fixed the instrument.
yosys sat -dump_jsonemits invalid JSONRTLIL names are written verbatim, backslashes and all.
formal/trace_reader.pyrepairs stray backslashes before parsing, and expands WaveJSON properly —.repeats the previous value,=consumes the nextdataentry. A reader that ignores.loses most of the trace: the same failure one layer down.Validated before use
The reader is pointed at a property whose counterexample is known — the prefetch with its clamp removed, which must show a write at a wrapped address. It parses 91 signals and finds the wrap at t=18. That check is a CI step.
With it working, the defect was legible immediately
The first query — not eyeballing, but asking at which timestep does the guard hold and the assertion fail — returned
t=28: local_addr=1, expected 0. The first write of a transfer was landing at address 1. Two mechanisms, both fixed:local_addrserved two roles — write pointer when data comes from the bus, read pointer when it goes to it. Prop. 29d gave only one role its own index, so the two fought. Both paths now share one sequential index.length != 0branch. A zero-length request takes the DONE path and left the pointers where the previous transfer put them. Reset now happens on every start.Still open, for a stated reason
After both fixes the property still refutes. That is the third patch; the rule from Prop. 29 — after two failed attempts, read the counterexample rather than patch again — was followed, produced two real defects, and did not exhaust the cause. It stays gated as an expected refutation. What changed is that the next investigation starts with a working instrument.
Both fixes were kept. Neither closed the target property, which by Prop. 25's standard is grounds for withdrawal. They were kept because each is independently correct and nothing regressed — module suites, engine baseline, 21 integration properties and the full zero-size sweep all pass.
31 propositions · 31 gates · 1212 passed, 0 failed · seals 496/496.
Three variants for the next wave
A — Finish the DMA with the working instrument. The next query is cheap now: dump the trace after the two fixes and find the third mechanism. Three waves of accumulated context plus a validated reader is the best position this item has ever been in.
B — Read-side pairing. Every property so far constrains writes. Nothing checks that an 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 — the mirror of the defect class that has produced four findings.
C — Point the reader at every existing refutation. Two open properties are gated as expected refutations, and each was diagnosed with the broken instrument or not at all. Re-read both traces now that the reader works; a gated refutation whose cause was never actually read is a finding waiting to be misfiled.