An error-correcting decoder in an open hardware library declared a syndrome output that nothing drove. A cover requirement added while proving the encoder and decoder pair found it; the one-line fix and the proof were reviewed and merged by the maintainer.

The system said: Interface: output syndrome_o. No check in the repository read it.
The evidence showed: Nothing drove it. A cover requirement in the first formal proof of the pair found it; the one-line fix and the proof were reviewed and merged upstream.

§ 1

The record

FINDING · ecc-decoder-syndrome-output-never-drivenverify · coverage illusion

An error-correcting decoder in an open hardware library declared a syndrome output that nothing drove. A cover requirement added while proving the encoder and decoder pair found it; the one-line fix and the proof were reviewed and merged by the maintainer.

Claim: In pulp-platform common_cells, cc_ecc_decode declared an output syndrome_o and never assigned it. The library had no proof or testbench for the encoder and decoder pair, so nothing exercised the port. While adding a SymbiYosys proof of the four properties documented in the decoder header, a cover requirement on syndrome_o showed the output was undriven; Verilator's lint reports the same. A one-line assignment fixed it, the proof and a width sweep to 64 bits passed with the fix, and the maintainer reviewed and merged the change on 3 September 2026.

Status: OBSERVED Witnessed in one instance. No claim about how often.

Question: Passed is not correct

Subject: pulp-platform common_cells, an open hardware IP library (third-party system); the proof harness is Omega's. third-party subject

Frame: Combinational encoder and decoder pair; prove and cover tasks under SymbiYosys with abc pdr; widths 1, 2, 4, 5, 11 and 12 by default.

Method: Four documented properties transcribed from the decoder header into assertions. One encoder feeds four decoders, each seeing a different corruption, so no case can weaken another. A cover task runs alongside the proof so a property resting on an unsatisfiable assumption cannot pass silently. Coverage of the syndrome output was added at the maintainer's request, and that is where the undriven output showed.

Oracle: The cover task: a documented syndrome value that cannot be reached is reported rather than passed. Verilator's undriven-signal lint agrees.

Negative control: Present An earlier version of the harness shared the error-position inputs across widths, which let one width's constraint narrow another's reachable positions while the proof stayed green. The cover task caught it, which is why it runs by default rather than on request.

Denominator: 1 undriven output; 4 properties at 6 default widths; 128 properties to width 64 in the sweep; 6 files changed in the merged pull request.

Limitation: One undriven output in one module of one library. The proof covers the pair at widths 1, 2, 4, 5, 11 and 12 by default and 128 properties up to width 64 in a sweep; it says nothing about the data output under a double error, nothing beyond two flipped bits, and nothing about other modules. The proof needs SymbiYosys, Yosys and abc; it was run by the author before and after the fix and reported in the pull request, and has not been re-run for this record. Maintainer acceptance is review of one change, not endorsement of Omega. The fix is on the default branch and in no tagged release as of 4 September 2026.

Source: pulp-platform/common_cells @ a257b714

Reproduce: cd formal && make ecc.check

Independent reproduction: None known. The maintainer's review is a review of the change, not a reproduction of the run.

Upstream: MERGED UPSTREAM Pull request #355, reviewed and merged by the maintainer on 3 September 2026. Link

§ 2

Where this sits

This finding answers Passed is not correct and supports the VERIFY stage of the operating method. It is an instance of the coverage illusion mechanism.

Evidence ledger Bring a claim like this one