Blog
A formal verification job stayed green its whole life while three independent mechanisms each guaranteed it could never go red — pseudo-syntax configs, a pipe that tested tee instead of the tool, and continue-on-error over everything. Peeling it to the first genuine proof took seven named layers, including RTL four months older than the compiler under test and property files that never instantiated the DUT. It ends with the repository’s first real formal verdicts: fifo and mac, Status PASSED under z3.
A formal verification job had been green for its entire life and had never run a solver. Not once. An adversarial audit of our own claims found it; peeling it down to the first genuine proof took seven distinct layers, each one invisible until the layer above it was cured. This is the anatomy, because every layer is a class of failure that exists in other people's pipelines too.
Three independent mechanisms each guaranteed green, so fixing any one of them changed nothing observable. The .sby configs used indented pseudo-blocks the tool does not parse, so every task died in milliseconds with a config error. The shell condition was 'if sby | tee log' — without pipefail, under bash -e, the if tests tee's exit status, which is always zero, so PASS was recorded unconditionally and the failure branch was unreachable code. And the job carried continue-on-error: true, so even a failing step could not redden the run. Green squared, then cubed.
The audit that caught it was mechanical: for each green job, ask what the log actually proves, and try to refute the claim 'this job verified something'. Two independent refuters each failed to refute; the finding survived. The same audit pass found a conformance job whose 'CLEAN' verdict was a static JSON field echoed into the summary as if computed, and a lint job that had absorbed the message 'NOT READY — fix parse errors first' from its own readiness tool, which printed the verdict and exited zero.
| layer | what was actually wrong | the general class |
|---|---|---|
| 1 | indented pseudo-blocks in .sby that sby reads as garbage | a config dialect is a contract; a plausible-looking example is not documentation |
| 2 | [files] paths climbing ../../../ out of the workspace | paths in configs resolve by the tool's rules, not yours |
| 3 | if sby | tee — the if tests tee | under set -e a pipeline's exit is its last stage; pipefail or lose every verdict |
| 4 | sby resolves [files] against the invocation cwd, not the .sby location | run the tool from where its config assumes it runs |
| 5 | read_verilog without the repo's dialect flags | every reader of generated code needs the same flags the rest of the repo uses |
| 6 | the copy chain preferred April-vintage committed .v files over the artifact generated minutes earlier in the same run | committed copies of generated files shadow silently; fresh output first, stale fallback loud, absence fatal |
| 7 | the property modules never instantiated the DUT — assertions floated over undriven mirror ports in SVA the tool cannot parse anyway | a property file that elaborates is not a property file that checks anything; the DUT instantiation is the first assertion |
Layer 6 deserves a pause: the formal job was testing RTL four months older than the compiler it was supposed to be testing. And layer 7 is the deepest kind — even under a full SVA tool, every assertion in those property files was vacuously true, because the ports they constrained were connected to nothing.
Layers 1 through 4 were paid for at forty-five minutes per lesson, one CI round-trip each. Layers 5 through 7 fell in minutes, because the tool's whole chain runs locally without the wrapper: yosys prep, write_smt2, yosys-smtbmc with z3 reproduces sby's core exactly. The last diagnosis rule that mattered: the engine failure's real name lives in the job's artifact — the per-task logfile.txt — while the job log only says 'engine did not return a status'. Download the artifact before theorizing.
$ yosys -q -p "read_verilog -formal -sv -DSIMULATION fifo.v; \
read_verilog -formal fifo_formal_props.v; \
prep -top fifo_formal_props; write_smt2 fifo.smt2"
$ yosys-smtbmc -s z3 -t 5 fifo.smt2
## 0:00:00 Status: PASSEDThe v1 property sets that replaced the floating ones are deliberately thin: they instantiate the real generated modules and assert what is actually provable about them today — for two of the three, that is a single handshake invariant, because the generated modules currently expose no data ports at all. Thin, but bound and proven: fifo and mac reach Status PASSED under z3, locally and then in CI. The first genuine formal verdicts in the repository's history.
The third module is parked, honestly: writing its property exposed a real design defect — a latch with combinational feedback that no SMT model accepts, inferred because the code generator lowers state writes inside a combinational context. The property file is written and its invariant is cross-checked by exhaustive simulation over all 256 input bytes; the config carries a .blocked suffix and the issue number. A parked config with a named cause beats both a deleted one and a green one.
A green gate is a claim about the gate, not about the design. The only way to know which one you have is to ask what a red result would have looked like — and if no reachable code path produces red, the green is measuring the shell, not the silicon. Audit your greens with the same hostility you audit your reds; the greens are where the surprises keep.
Every figure above is measured, and the limits are named with it.