Free-form drift and its cure: what a renamed interrupt port taught us

The problem

Ask an LLM to turn a natural-language brief into SystemVerilog and it will oblige - producing code that compiles, simulates, and is wrong in ways invisible until something exercises the exact path that drifted. The failure mode is not a crash. It is a signal that quietly stops meaning what everyone assumed it meant.

We build against this with Architectural Pre-Commitment: freeze the microarchitecture contract before any RTL is written, so the model’s job collapses to filling strictly defined slots. Here is a real case where pre-commitment did not stop the drift - it just made the drift a locatable, provable finding instead of a silent one. That is a more honest claim, and it is the one the evidence actually supports.

Show the failure

The contract for axis_fifo_csr - a FIFO datapath behind an AXI4-Lite CSR block - names its interrupt output in the ComponentSpec port table:

Name	Dir	Interface	Description
irq_o_irq	out	irq_o	Active-high, level-sensitive, fully synchronous interrupt request equal to OR-reduction of masked INT_STATUS.

The generated RTL’s top-level port list names the same signal differently:

module axis_fifo_csr (
    // ...
    // Interrupt output
    output logic        irq_o
);

Both are internally consistent - the RTL wires its own irq_o port straight through to its child’s irq_o port correctly. The mismatch is not inside the RTL. It is between the RTL and the contract that described it, and it surfaces one stage later, in the formal harness generated from the contract:

    logic        irq_o_irq;
    // ...
    axis_fifo_csr u_dut (
        // ...
        .irq_o_irq      (irq_o_irq)
    );

The harness was generated faithfully from the ComponentSpec, so it uses the ComponentSpec’s name. The DUT has no port called irq_o_irq. The named connection does not bind to anything real, and irq_o_irq inside the harness is left floating.

Key Lesson: A generated artifact that is faithful to its contract is not the same as an artifact that is faithful to the other generated artifact next to it. Two things can each be internally consistent and still disagree with each other.

Why it fails

Yosys’s elaboration pass catches the dangling wire immediately, twice, once per property file that references it:

Warning: Wire fv_axis_fifo_csr_top.\u_dut.irq_o_irq is used but has no driver.
Warning: Wire fv_axis_fifo_csr_top.\u_dut.irq_o_irq is used but has no driver.

But an elaboration warning is not a failed proof, and that gap is exactly the mechanism worth seeing:

Layer	What it says	What actually happened
ComponentSpec (contract)	port is irq_o_irq	authoritative source of truth
RTL (axis_fifo_csr.sv)	port is irq_o	drifted from the contract’s name
Formal harness (generated from contract)	wires irq_o_irq to the DUT	connection does not bind - net floats, tied to 1'b0
Reset-idle assertion on that net	passes	vacuously - the net it checks is never driven
Cover on that net	never witnesses	the signal it is meant to observe cannot change

The reset-idle assertion for the interrupt genuinely never fails, at any BMC depth. It just was not testing anything - the exact vacuity trap a green formal result can hide.

Key Lesson: “The assertion passed” and “the assertion was ever at risk of failing” are different claims. A floating net satisfies the first without coming near the second.

The fix

The fix itself is small and precisely scoped: reconcile the harness’s DUT-facing port name with the RTL’s actual, compiled port name, so the named connection binds to a real signal instead of a phantom one. What is not small is the implication - the contract and the RTL disagree, and something upstream of the formal stage has to decide which one is right and correct the other. The evidence pack recorded this as a documented, MEDIUM-severity, RTL-revision-class finding, not something the formal stage patches around itself. As of this run, that revision has not landed - the honest status is documented and open, not fixed.

Two ways to build the harness

There are two legitimate ways to generate a formal harness for a block like this, and this incident is the argument for picking carefully between them.

Generate the harness from the contract. This is what happened here. Pro: the harness can exist before the RTL does, and it encodes the intended architecture, not whatever the RTL happens to have been built as. Con: if the RTL drifts from the contract - as it did, on one port name - the harness faithfully reproduces the contract’s expectation, tries to wire a signal that is not there, and produces a dangling connection instead of a real check.

Generate the harness from the RTL’s actual port list. Pro: the named connection always binds, because the harness always asks the RTL what it is actually called. This specific dangling-wire failure mode cannot happen. Con: you lose the one thing a contract-derived harness buys you - the ability to notice that the RTL stopped matching what was asked for. A harness introspected from the RTL will happily wire up whatever the RTL renamed itself to and call it correct.

Neither approach alone is sufficient. The real fix implied by this finding is a third, cheaper check that neither harness style does today: a structural name-equivalence pass between the ComponentSpec’s port table and the RTL’s compiled port list, run before either the harness or the proof exists - a lint gate on the contract itself, not on its consequences three stages downstream.

Key Lesson: Choosing what a generated artifact is derived from is choosing what kind of drift it can catch. A contract-derived check catches spec-vs-implementation drift and misses nothing about intent; an implementation-derived check catches nothing about intent and never dangles.

Proving it

The full picture from proof-results.md: 23 assertions, 13 assume cells (12 labelled plus one anonymous reset assumption, deduplicated by Yosys across two property files), and 17 covers, run in BMC mode at depth 32, per this proof configuration - status PASS_WITH_WARNINGS, not a hard failure. The reset-idle family this bug lives in reads like this in the harness:

always @(posedge clk_i) begin
    if (!rst_n_i) begin
        A_STR_S_AXIS_TREADY_RST_IDLE_A: assert(S_AXIS_TREADY  == 1'b0);
        A_STR_M_AXIS_TVALID_RST_IDLE_A: assert(M_AXIS_TVALID  == 1'b0);
        A_STR_AXIL_AWREADY_RST_IDLE_A:  assert(S_AXIL_AWREADY == 1'b0);
        A_STR_AXIL_WREADY_RST_IDLE_A:   assert(S_AXIL_WREADY  == 1'b0);
        A_STR_AXIL_BVALID_RST_IDLE_A:   assert(S_AXIL_BVALID  == 1'b0);
        A_STR_AXIL_ARREADY_RST_IDLE_A:  assert(S_AXIL_ARREADY == 1'b0);
        A_STR_AXIL_RVALID_RST_IDLE_A:   assert(S_AXIL_RVALID  == 1'b0);
        A_STR_IRQ_RST_IDLE_A:           assert(irq_o_irq      == 1'b0);
    end
end

Seven of those eight assertions are checking a real signal driven by real DUT logic. The eighth, A_STR_IRQ_RST_IDLE_A, is checking a net the DUT never touches. Every one of them is labeled PASS in the same table. The cover that was supposed to be the tell - COV_IRQ_P: cover(irq_o_irq); in the companion covers file - never witnesses, and the record says exactly why rather than burying it in an aggregate pass count. This is the same discipline as grading a proof by its mutation kill rate instead of its raw pass count: a clean-looking result still has to earn the word “verified” for the specific thing it claims to cover, and this one, for the interrupt path specifically, has not.

From “it works” to “it ships”

• Reset: seven of the eight output-idle-on-reset properties are backed by real, driven signals and mean what they say; the interrupt one currently does not, and that gap is now a named, tracked finding rather than an invisible one.
• X-propagation: the block-wide $isunknown check over the same control outputs, including the interrupt net, also passes - Yosys ties the undriven wire to a constant 0 rather than X, so this check cannot see the problem either. Two independent-looking passing checks were both blind to the same root cause.
• Clock/reset domains: single clk_i domain, synchronous active-low rst_n_i - no CDC to account for at this hierarchy level.
• Contract closure: the RTL-revision fix is documented and open, not merged - stated exactly as that, not rounded up.

Lessons

Architectural Pre-Commitment did what it was supposed to do here: it did not stop the contract and the RTL from disagreeing, but it made that disagreement land as one dangling wire and one MEDIUM-severity warning with a file and a line, instead of a silent gap nobody would have gone looking for. The uncomfortable half of the lesson is that two different passing checks - a reset-idle assertion and an X-propagation check - were both fooled by the same undriven net, because neither one asks “is this signal actually connected to anything,” only “does this signal, whatever it is, currently behave.”

Where to go next

This is the same vacuity shape covered from the formal-methodology side in What a formal “PASS” has to earn - an assumption or a dangling connection can make a property true for reasons that have nothing to do with the design being correct. And it’s the same “ask for the file, not the summary” habit from The evaluator’s checklist, explained: the pass/fail table said PASS; the warning three sections down said why that PASS didn’t cover what it looked like it covered.

Can I re-run your proofs in my CI?