OBSERVED
Finding · verify
Two injected hardware defects passed every property written from the original specification, because the specification never stated the requirement they break.
- The system said
- All 26 requirement-derived assertions pass the unbounded proof.
- The evidence showed
- Two injected defects passed every property, because the specification never stated the requirement they break. Two of the 26 assertions are vacuous and cannot fail on any input.
§ 1
The record
FINDING · spcu-defects-passed-every-propertyverify · faithfulness
Two injected hardware defects passed every property written from the original specification, because the specification never stated the requirement they break.
- Claim
- Five defects were injected into a small power-control design whose formal verification argument was complete and green. Two of them passed every property derived from the original specification: one because the specification required voltage to be sufficient and never minimal, one because a two-step transition is internally consistent. A third escaped every property about the design's own variables while recording something false about the physical world.
- Status
- OBSERVED Witnessed in one instance. No claim about how often.
- Subject
- A small DVFS power-control IP written for the study (authored), verified with open tools. built for the study
- Frame
- 26 requirement-derived assertions; PDR unbounded proofs on a collapsed-clock model with four environment assumptions; clock-crossing checks bounded at depth 20; 2 assertions vacuous; 3 rest on a further stated assumption.
- Method
- Formal (SymbiYosys), Verilator simulation, a pyuvm testbench and bare-metal C against the RTL; five hand-injected defects, then 200 netlist mutations checked against the property set and an equivalence miter.
- Oracle
- The property set itself, then a mutation harness that asks which mutants any property can see; an equivalence miter separates no-op mutants.
- Negative control
- Present The 200-mutant mcy run: 84 covered, 23 equivalent, 93 in the gap. Vacuous assertions are kept and excluded from every claim.
- Denominator
- 2 of 5 injected defects passed every specification-derived property; 26 assertions, 2 vacuous; 200 mutants, 93 unseen.
- Limitation
- A claim about this ~450-line design and this property set only. The five mutations were written by the same person who wrote the properties; a 200-mutant Yosys run was added for that reason and showed the hand-written mutations had probed the wrong part of the design. Nothing here is a statement about any commercial verification flow.
- Source
- repowazdogz-droid/spcu-verification @ e49a0c5
- Reproduce
make setup && make all
- Independent reproduction
- None known.
§ 2
Where this sits
This finding answers The specification proved is not the property intended and supports the VERIFY stage of the operating method. It is an instance of the faithfulness mechanism.