☣️ [VERDICT]
Prop. 34b named weight_prefetch_ctrl as the one module whose proof does not extend — intractable at twice its bound, and therefore the one place a deeper defect could sit unseen. That was a fact about how it was asked, not about the module.
Individually decidable, jointly intractable
-prove-asserts solves every assertion of a module in a single SAT instance. At -seq 40:
| property |
verdict |
time |
a_sanity |
PROVED |
0.2 s |
a_no_overwrite |
PROVED |
87.2 s |
a_rready_implies_active |
PROVED |
0.4 s |
| all three together |
undecided |
>240 s |
The parts sum to under 90 seconds; the whole exceeds 240. The combined instance is superlinearly harder than its pieces.
Two consequences
Splitting raised the bound this module is verified at from 14 to 40 for the same wall time. CI now proves each property in its own invocation — and a batch that goes red says something in here broke, while per-property invocations name it.
And the reporting one:
A suite-level verdict tells you about its worst member and nothing about the rest. Reporting one number for this module concealed that two of its properties hold at -seq 80 while the third stops at 40. Where members differ by two orders of magnitude in cost, the aggregate is dominated by one and describes none of the others.
A cheaper decomposition was attempted and withdrawn
a_no_overwrite bounds a 17-bit counter against a 16-bit input, forcing the solver to carry that counter across the whole unrolling. The intended replacement was a local invariant — writes == bram_addr + 1 — leaning on max_size_props for the address never wrapping: a local invariant plus an existing property, in place of one global count.
It refuted in 0.5 s, twice, on the alignment between a counter registered off bram_we and an address assigned from word_index on the same edge. The idea is sound; the alignment is not established. Withdrawn and recorded rather than guessed a third time.
Narrowed, not closed: a_no_overwrite is proved at -seq 40 and undecided at 80. It remains the shallowest-verified property in the design — now stated per property rather than per module.
35 propositions · 35 gates · 1213 passed, 0 failed · seals 496/496 · no known defect open.
Three variants for the next wave
A — Split every batched suite. Only weight_prefetch_ctrl was split. The other four module suites and the 23-property engine set are still single invocations, so each reports the minimum over its members and each may be leaving depth on the table. Measuring per-property ceilings across the whole design turns one aggregate number into a map of where verification is actually shallow.
B — Establish the counter/address alignment and finish 35c. The withdrawn decomposition would make the design's most expensive property cheap. What is missing is one fact: the exact sampling relation between writes, bram_we and bram_addr. A short directed check — assert the relation at each candidate offset and see which proves — settles it without guessing.
C — Read-side pairing. Still the largest unexamined surface, and untouched for four waves. Every property constrains writes; a read-enable held across states, a read address sampled a cycle off, or a read of a slot before its layer wrote it all have zero coverage.
☣️ [VERDICT]
Prop. 34b named
weight_prefetch_ctrlas the one module whose proof does not extend — intractable at twice its bound, and therefore the one place a deeper defect could sit unseen. That was a fact about how it was asked, not about the module.Individually decidable, jointly intractable
-prove-assertssolves every assertion of a module in a single SAT instance. At-seq 40:a_sanitya_no_overwritea_rready_implies_activeThe parts sum to under 90 seconds; the whole exceeds 240. The combined instance is superlinearly harder than its pieces.
Two consequences
Splitting raised the bound this module is verified at from 14 to 40 for the same wall time. CI now proves each property in its own invocation — and a batch that goes red says something in here broke, while per-property invocations name it.
And the reporting one:
A cheaper decomposition was attempted and withdrawn
a_no_overwritebounds a 17-bit counter against a 16-bit input, forcing the solver to carry that counter across the whole unrolling. The intended replacement was a local invariant —writes == bram_addr + 1— leaning onmax_size_propsfor the address never wrapping: a local invariant plus an existing property, in place of one global count.It refuted in 0.5 s, twice, on the alignment between a counter registered off
bram_weand an address assigned fromword_indexon the same edge. The idea is sound; the alignment is not established. Withdrawn and recorded rather than guessed a third time.Narrowed, not closed:
a_no_overwriteis proved at-seq 40and undecided at 80. It remains the shallowest-verified property in the design — now stated per property rather than per module.35 propositions · 35 gates · 1213 passed, 0 failed · seals 496/496 · no known defect open.
Three variants for the next wave
A — Split every batched suite. Only
weight_prefetch_ctrlwas split. The other four module suites and the 23-property engine set are still single invocations, so each reports the minimum over its members and each may be leaving depth on the table. Measuring per-property ceilings across the whole design turns one aggregate number into a map of where verification is actually shallow.B — Establish the counter/address alignment and finish 35c. The withdrawn decomposition would make the design's most expensive property cheap. What is missing is one fact: the exact sampling relation between
writes,bram_weandbram_addr. A short directed check — assert the relation at each candidate offset and see which proves — settles it without guessing.C — Read-side pairing. Still the largest unexamined surface, and untouched for four waves. Every property constrains writes; a read-enable held across states, a read address sampled a cycle off, or a read of a slot before its layer wrote it all have zero coverage.