The solver is a hallucination filter

An automated review pass read a specification, checked it against a brief, and signed off clean: 0 critical findings, 0 warnings. Two of the citations it approved pointed to requirement IDs that do not exist anywhere in the document. This is what happened, why it happened, and why a formal solver checking the resulting RTL cannot fail in the same way - and exactly where its guarantee runs out.

The problem

If you use an LLM to write a spec, review a spec, or summarize whether a design meets a spec, you inherit a question you cannot dodge: how do you know “looks compliant” is not standing in for “is compliant”? A model that writes fluent, well-formed text can write a fluent, well-formed citation to something that was never there. That is not a hypothetical risk. It happened, twice, in the same pipeline, on the same afternoon.

Show the failure

Stage 2 of a production RTL-generation run produces an architecture document, then routes it through automated reviewers before a human ever reads it. One reviewer covers external interfaces; another covers the block decomposition. Both reviewers read the same artifact. Only one of them caught this:

What the document cited	What actually exists
REQ-CLK-01 (clock interface purpose)	No such ID. Real requirement is REQ-CLK-100.
REQ-RST-01 (reset interface purpose)	No such ID. Real requirement is REQ-CLK-110.

Both invented IDs follow the house naming grammar exactly - REQ-<DOMAIN>-<NUMBER> - so they read as obviously legitimate. The external-interface reviewer produced 8 info-level findings on that same document and did not flag either one. The decomposition reviewer, auditing a different file that referenced the same two IDs, caught the fabrication and marked it CRITICAL. A human review pass patched both citations before the architecture advanced to hierarchy.

One stage earlier, a related miss: Stage 1’s automated review built a 25-entry brief-to-requirement coverage matrix and marked every entry status: full - 0 critical, 0 warning findings, on first attempt. The matrix was wrong about one thing: it let all five interrupt sources become rising-edge-triggered, when the brief only tagged one of them that way for the other four, the correct reading is level-sensitive. The matrix still said full, because it was checking that a covering requirement ID existed for each brief item, not that the requirement’s stated behavior matched the brief’s behavior. A human comparison pass, reading the brief and the spec side by side, caught it before any RTL existed.

Key Lesson: “It passed review” and “review was capable of catching this” are different claims. Both of these passed clean, and that is exactly when a fabrication or a semantic drift is most dangerous - nothing downstream is watching for it.

Why it fails

Both misses share a mechanism. An LLM-based reviewer, whether it is generating the artifact or auditing it, is making a plausibility judgment: does this citation have the right shape, does this coverage matrix have the right counts, does this sentence sound like it satisfies the requirement it’s attached to. None of that is an existence check against ground truth.

Check performed	What it verifies	What it misses
Coverage matrix (Stage 1)	A requirement ID exists for each brief item; counts match	Whether the requirement’s behavior matches the brief’s behavior
External-interface review (Stage 2)	The interface description reads as complete and well-formed	Whether the requirement IDs it cites are real
Decomposition review (Stage 2)	Cross-checks requirement IDs against the actual 53-entry requirements table	Nothing in this case - this is the one that caught it

The reviewer that caught the fabrication did one additional thing the other two did not: it checked the cited ID against the actual list of IDs that exist, rather than judging whether the citation read as plausible. That is the whole difference between a fidelity check and a completeness check, and it is not a difference in effort or model quality - it is a difference in what question was asked.

Key Lesson: A hallucination is not “the model was careless.” It is a plausibility judgment standing in for an existence check, and it will keep happening anywhere that substitution is possible - which is anywhere the check is made of natural language.

The fix, line by line

Somewhere downstream, that same interrupt-semantics question - is this level-sensitive or edge-triggered, and does the output actually track it - stops being a sentence a reviewer judges and becomes a property a solver checks against the compiled netlist. Here is the real bound property from csr_control_plane’s formal harness:

// IRQ no-phantom: $past of the multi-bit (status & mask) OR-reduction.
// R-INT-NO-PHANTOM requires that irq_o only asserts if (status & mask)
// was non-zero in the previous cycle. We sample the OR-reduction as a
// 1-bit shadow.
reg _shadow_status_mask_or_q;
always @(posedge clk_i) begin
    if (!rst_n_i) begin
        _shadow_status_mask_or_q <= 1'b0;
    end else begin
        _shadow_status_mask_or_q <=
            (int_status_overflow_r        & int_mask_overflow_r) |
            (int_status_underflow_r       & int_mask_underflow_r) |
            (int_status_packet_received_r & int_mask_packet_received_r);
    end
end

// R-INT-NO-PHANTOM [HIGH] irq_o only asserts if any (status & mask) was 1 in prev cycle
always @(posedge clk_i) begin
  if (rst_n_i) begin
    assert_irq_no_phantom_A: assert(!irq_o || _shadow_status_mask_or_q);
  end
end

// R-INT-LEVEL-POLARITY [HIGH] irq_o equals registered OR-reduction of (status & mask).
always @(posedge clk_i) begin
  if (rst_n_i) begin
    assert_irq_level_polarity_A: assert(irq_o == _shadow_status_mask_or_q);
  end
end

Neither property reads a citation and neither one is graded on how plausible it sounds. assert_irq_level_polarity_A is a claim about the compiled netlist’s reachable states: on every clock edge, irq_o equals the registered OR-reduction of masked status, full stop. A solver checking that claim does not have a “looks right” outcome available to it. Given the property and the design, it either derives that no reachable state violates it - up to the depth or induction bound configured - or it produces a concrete counterexample: a specific cycle, specific register values, a specific trace where the equality breaks. There is no third answer where it rates the claim compliant because the label assert_irq_level_polarity_A has the right shape, the way REQ-CLK-01 had the right shape.

Key Lesson: A solver cannot be fooled by something that merely looks correct, because it never evaluates “looks” at all. It evaluates whether a state exists. That is a narrower question than “is this design good” - and a strictly more answerable one.

Two ways to build it

Bounded model checking (BMC). csr_control_plane’s formal harness runs in BMC mode at depth 50, chosen because - per the harness’s own mode rationale - the block’s primary archetype is a controller, not one of the FSM/FIFO/counter shapes the pipeline keeps an induction shadow model for. BMC at that depth covers every FSM transition and every AXI-Lite handshake completion from any legal pre-reset state, within a 50-cycle window. Pro: cheap, fast, and it is exactly what caught the reset-property mismatch elsewhere in this same run (see “Where to go next”). Con: a bug that only manifests past cycle 50 is invisible to it by construction.

K-induction. Where a design carries clean internal state to induct over (a FIFO’s occupancy counter, an arbiter’s grant register), induction proves a property for arbitrarily many cycles, not just within a bound - a strictly stronger claim. Con: it needs a decidable induction step, which usually means hand-adding shadow-model help, and some open-source toolchains silently degrade it back to BMC when they can’t expose the internal state (this exact block’s sibling, fifo_datapath, hit that limitation - see “From it works to it ships” below).

Neither mode changes the underlying guarantee: whichever one closes, the answer is UNSAT-up-to-bound or a counterexample, never a paragraph of hedged confidence.

Proving it

When one of these two properties fails, the solver’s response is not prose. It is a trace: the exact cycle reset deasserts, the exact write to INT_MASK, the exact point where irq_o and _shadow_status_mask_or_q disagree, and the value of every signal along the way, reproducible on demand. That shape of answer - a specific falsifying assignment, not a rated likelihood - is what a fabricated citation can never produce, because a fabrication has no state space to be wrong about.

It is also worth being honest about the boundary. BMC at depth 50 proves these two properties hold for any legal input sequence within that window, from a single symbolic starting point. It says nothing about sustained, randomized, multi-thousand-beat traffic, or about INT_STATUS write-one-to-clear racing a live interrupt source under real timing variance. That is exactly what the same block’s UVM regression is for: axis_fifo_int_status_w1c_race_test (REQ-FUNC-014) drives an interrupt source to fire on the same cycle as a W1C write and checks the bit survives; axis_fifo_irq_timing_test (REQ-FUNC-013) sets status bits individually through randomized AXI4-Lite transactions and checks irq_o asserts and deasserts on schedule under live sequencing formal never drives. Formal and simulation are checking the same interrupt path from two different angles, on purpose, because neither one covers the other.

Key Lesson: “The property is proven” and “the block is done” are different claims. A bound proof plus an unexercised traffic pattern is still an open question - which is why the pipeline runs both stages on the same design, not one instead of the other.

From “it works” to “it ships”

• Reset: proven at BMC depth 50 for FSM transitions and handshake completion from any legal pre-reset state (csr_control_plane proof record).
• Induction honesty: state which properties closed by induction versus BMC, and say so plainly when a toolchain limitation forces a downgrade - fifo_datapath’s induction-strengthening internal signals were invisible to the open-source elaboration pass in that run, so its shadow-model properties dropped to a bounded, port-level check instead, and the record says exactly that rather than rounding up.
• Two-layer review for anything expressed in natural language: a completeness check (does a covering ID exist) is not a fidelity check (does the ID’s content match the source); running only one is how a fabricated citation survives to the next stage.
• Clock/reset domains: single clk_i, synchronous active-low rst_n_i - no CDC to account for at this hierarchy level.

Lessons

Natural-language review checks whether something looks right. A solver checks whether it is possible for it to be wrong, given the property you actually wrote. Those are different questions, and rerunning the same kind of check with more care only ever answers the first one.

Formal earns its guarantee by being narrow - one property, one bounded or inductive claim, over one compiled design’s reachable states - never by being the whole verification story. The honest sign-off names its bound, its engine, and the traffic patterns it never drove.

The bundle

The requirements, architecture, and formal artifacts referenced here are from a real, staged RTL-generation run; the review outcomes and the property source shown above are quoted directly from that run’s records, not reconstructed from memory. For how VoskenAI grades a formal pass beyond “it ran” - vacuity, engine honesty, mutation testing - see /evidence and the posts below.

Where to go next

What a formal “PASS” has to earn covers the other side of this coin: a property that runs clean but was never at risk of failing. Free-form drift and its cure is the same pipeline’s other documented case of a contract-versus-implementation mismatch, caught downstream by the formal stage instead of upstream by review. A follow-up on grading the verification itself with mutation testing - how you know your checks would actually catch a real defect - is next in the queue.

Can I re-run your proofs in my CI?