Cases / Chip design
A chip component had an output wired to nothing, and its tests didn’t notice
- It said
- Four automated checks passed. (They were mine: the first ever written for this component.)
- Actually
- One of its outputs wasn’t connected to anything.
- Then
- An extra check the maintainer asked for showed it. My one-line fix was accepted.
PULP common_cells is an open-source library of chip components. One component, an error-correcting decoder, was meant to report where an error is on one of its outputs. Nothing was connected to that output, and its existing test never looked at it.
The technical record
My first formal proof of the module: four documented properties, proved.
One declared output, syndrome_o, was never connected. A cover check the maintainer asked for found it.
An error-correcting decoder in an open-source hardware library declared an output meant to report where an error is. Nothing drove it. The library had no formal proof of the module, and its existing testbench never read that output, so nothing noticed. I wrote the first formal proof for it, and a cover check on that output showed it could never be set. My one-line fix and the proof were merged.
What a green proof did and didn’t see
Choose what the formal tools were asked to do.
syndrome_o ever be set?Not askedEverything is green. Nothing has looked at syndrome_o.
How the finding was reached
Claim
The decoder reports the position of a corrected error on
syndrome_o.Test
I transcribed the four properties documented in the decoder header into a SymbiYosys proof: one encoder feeding four decoders, each seeing a different corruption, at widths 1, 2, 4, 5, 11 and 12.
What happened
All four properties proved. A cover requirement on
syndrome_o, added at the maintainer’s request, could not be reached: the output was declared and never assigned. Verilator’s lint agreed.Trying to break the finding
Why trust a green proof at all? An earlier version of my own harness shared error-position inputs across widths, which let one width narrow another while the proof stayed green. A cover task caught that, which is why cover now runs by default rather than on request.
Evidence
A one-line assignment fixed the output. The proof, and a sweep to width 64 (128 properties), passed with the fix. The maintainer reviewed and merged it on 3 September 2026.
What survives
Passing properties said nothing about an output that no property read. The cover check is what made the gap visible.
What this does not show
One undriven output in one module of one library. Nothing is claimed beyond two flipped bits or about other modules. The proof was run by me before and after the fix and has not been re-run for this page. The fix is on the main branch; the latest stable release (v1.40.0) and pre-release (v2.0.0-beta.3), both from July 2026, predate it.
If this had been your system
If this were your design, you would have received the proof harness, the cover results, the fix, and a CI job that fails if any declared output becomes unreachable.