Artifact
spcu-verification
A small power-control IP verified with open tools; two injected defects invisible to every specification-derived property.
What it establishes
That a complete, green formal argument over a small DVFS controller left two of five injected defects undetected because the specification never stated the requirement they violate, and that a 200-mutant run showed the hand-written mutations had probed the wrong part of the design.
What it does not establish
Anything about commercial flows or larger designs. The mutations and the properties share an author. Unbounded proofs are separated from bounded checks and vacuous assertions are excluded from every claim.
Method
Formal proofs (PDR), simulation, a UVM-architecture Python testbench and bare-metal C against the RTL; five injected defects; 200 netlist mutations checked against the property set and an equivalence miter.
Results
26 requirement-derived assertions pass the prove task, 2 vacuous, 3 resting on a further stated assumption; four unseeded design bugs found by formal; 200 mutants: 84 covered, 23 equivalent, 93 in the gap.
What has to be trusted
Yosys, SymbiYosys, ABC, Z3, Verilator, cocotb and pyuvm; the collapsed-clock model and its four environment assumptions; the hand-written specification.
Prior work
Mutation analysis for formal property sets and specification adequacy. The contribution is the worked, open-tool instance with the vacuous assertions kept in view.