☣️ [VERDICT]
Prop. 35 split one module and found its aggregate verdict was hiding its members. This maps the rest — every property of every module suite, isolated, at 1×, 2×, 4× and 8× the bound it is checked at.
Not every suite is bounded
Two of the six run sat -tempinduct, which proves by k-induction and therefore holds for all time, not to a depth:
| suite |
mode |
what -seq means |
interrupt_controller |
-tempinduct |
induction depth — proof is unbounded |
axi_lite_slave |
-tempinduct |
induction depth — proof is unbounded |
dma_controller |
bounded BMC |
a ceiling |
layer_sequencer |
bounded BMC |
a ceiling |
weight_prefetch_ctrl |
bounded BMC |
a ceiling |
bitnet_engine_top |
bounded BMC |
a ceiling |
Prop. 34's scale-ceiling framing does not apply to the first two. Worse, my map measured them with plain BMC and reported "proved at 8× the CI bound", which understates them — they are proved without any bound at all.
Before measuring how far a result extends, check whether it is the kind of result that extends. The two modes differ by one flag, and nothing in the aggregate output says which produced the verdict.
The near-mistake this caused
Acting on "everything proves at 4× for under 8 seconds", I raised the CI bounds — including axi_lite_slave from 10 to 80. For a -tempinduct run that is not a strengthening: the proof is already unbounded and -seq is the induction depth, so the only effect is cost. Reverted.
A number that means one thing in one mode means something else in another, and the parameter has the same name in both.
The bounded suites have enormous headroom
| suite |
properties |
deepest PROVED (isolated) |
slowest |
dma_controller |
7 |
≥160 (8× CI bound) |
8.8 s |
layer_sequencer |
4 |
≥96 (8×) |
50.0 s |
weight_prefetch_ctrl |
3 |
2 at ≥80, 1 at 40 |
87.2 s |
"≥" because 8× was the sweep's own cap, not the properties' limit. Only a_no_overwrite has a measured ceiling below the cap.
Bounds raised where meaningful: dma_controller 12 → 80 (3.6 s) and layer_sequencer 12 → 48 (9.8 s), both verified — 6.7× and 4× deeper verification for about thirteen seconds of CI time.
What the map is worth: verification was six numbers, two of which meant something different from the other four and one of which was the minimum over three wildly different members. Now every property has a measured depth. The aggregate was not wrong; it was uninformative in a way that looked informative.
36 propositions · 36 gates · 1213 passed, 0 failed · seals 496/496 · no known defect open.
Three variants for the next wave
A — Convert the bounded suites to induction. Two suites already prove unboundedly, so the technique is in the repo and works on this design. dma_controller and layer_sequencer have vast BMC headroom, which is exactly the profile of a property that k-induction can close. Converting them replaces "proved to depth 80" with "proved, full stop", and retires the scale-ceiling gate for those suites entirely.
B — Finish the engine per-property map. The 20-property engine set is still a single bounded verdict at -seq 40, and the batch is undecided at 80. Isolating them will show which properties are genuinely shallow and which are being dragged down by one expensive neighbour — the same discovery Prop. 35 made at module scale.
C — Read-side pairing. Still untouched after five waves, and still the largest unexamined behavioural surface. 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. 35 split one module and found its aggregate verdict was hiding its members. This maps the rest — every property of every module suite, isolated, at 1×, 2×, 4× and 8× the bound it is checked at.
Not every suite is bounded
Two of the six run
sat -tempinduct, which proves by k-induction and therefore holds for all time, not to a depth:-seqmeansinterrupt_controller-tempinductaxi_lite_slave-tempinductdma_controllerlayer_sequencerweight_prefetch_ctrlbitnet_engine_topProp. 34's scale-ceiling framing does not apply to the first two. Worse, my map measured them with plain BMC and reported "proved at 8× the CI bound", which understates them — they are proved without any bound at all.
The near-mistake this caused
Acting on "everything proves at 4× for under 8 seconds", I raised the CI bounds — including
axi_lite_slavefrom 10 to 80. For a-tempinductrun that is not a strengthening: the proof is already unbounded and-seqis the induction depth, so the only effect is cost. Reverted.A number that means one thing in one mode means something else in another, and the parameter has the same name in both.
The bounded suites have enormous headroom
dma_controllerlayer_sequencerweight_prefetch_ctrl"≥" because 8× was the sweep's own cap, not the properties' limit. Only
a_no_overwritehas a measured ceiling below the cap.Bounds raised where meaningful:
dma_controller12 → 80 (3.6 s) andlayer_sequencer12 → 48 (9.8 s), both verified — 6.7× and 4× deeper verification for about thirteen seconds of CI time.What the map is worth: verification was six numbers, two of which meant something different from the other four and one of which was the minimum over three wildly different members. Now every property has a measured depth. The aggregate was not wrong; it was uninformative in a way that looked informative.
36 propositions · 36 gates · 1213 passed, 0 failed · seals 496/496 · no known defect open.
Three variants for the next wave
A — Convert the bounded suites to induction. Two suites already prove unboundedly, so the technique is in the repo and works on this design.
dma_controllerandlayer_sequencerhave vast BMC headroom, which is exactly the profile of a property that k-induction can close. Converting them replaces "proved to depth 80" with "proved, full stop", and retires the scale-ceiling gate for those suites entirely.B — Finish the engine per-property map. The 20-property engine set is still a single bounded verdict at
-seq 40, and the batch is undecided at 80. Isolating them will show which properties are genuinely shallow and which are being dragged down by one expensive neighbour — the same discovery Prop. 35 made at module scale.C — Read-side pairing. Still untouched after five waves, and still the largest unexamined behavioural surface. 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.