DATE 2027 · direction proposal · 3 August 2026

Ask the model k times.
Let a solver decide if the answers are the same circuit.

A reference-free, testbench-free correctness signal for LLM-generated Verilog. At zero false alarms it catches 95.5% of problems containing a wrong implementation. Every cheap text heuristic catches under 8%. Everything below ran on a MacBook Air with yosys and no paid API.

P. Khosh Solat · M. Hassan · M. Taheri · R. Drechsler 1,248 generations 110 problems scored clean cost: 0 EUR

The decision I need on Monday

Adopt formal sample-agreement as the DATE 2027 direction, and give me one week for the causal experiment.

The instrument works and beats every cheap alternative with a significant margin. What is not yet proven is the causal claim: that adding a missing sentence to a specification repairs the failure. That is a one-week experiment with a clear kill gate. If the placebo row is not null, I stop and tell you.

Specific ask for Rolf's group: 26 of 156 problems were dropped because they are sequential circuits with no reset, so there is no defined start state. I have an untested zero-init contract. Does the group have a better sequential equivalence flow? That is where your expertise buys us 25% coverage directly.

Where the old direction went

Input drift is dead, in one line

The drift score was computed from text alone and never touched the model, so it could not be a statement about model competence. On ResBench, design category by itself explains R² = 0.610 of pass-rate variance across nine commercial models; specification length explains 0.016; the drift score adds nothing significant on top of category. That line of work is closed. Everything below is new.

Figure 1 · the method

What the system does

In deployment there is no golden model and no testbench, so the usual correctness oracles are unavailable. The signal is built instead from the model's disagreement with itself, adjudicated formally rather than by simulation.

Specification English, 1 sentence+ LLM × k k=8, T=0.8 candidate 1 candidate 2 ⋮ candidate k Verilog, all textually different yosys + SAT pairwise formal equivalence check “same output for every possible input?” nothing else in the loop no testbench no golden reference no LLM as judge partition 1 class → ACCEPT all k compute the same circuit empirically 93.6% all-correct >1 class → REJECT at most one class can be right, so ≥1 candidate is wrong. sound by construction solver returns the exact input → read off the missing spec fact → add sentence, regenerate, measure Δ

Two properties carry the whole argument. Soundness is free: if the k answers compute different functions, at most one can match intent, so at least one is wrong. That is a theorem, not a threshold. No language model sits in the measurement path: the model proposes, only the solver judges.

Figure 2 · the experiment

How we tested whether it actually works

Two measurements, kept strictly independent. One consults the golden reference and is used only for grading. The other never sees it, matching the deployment condition.

VerilogEval v2 156 problems each ships a golden answer qwen2.5-coder:7b local, 8 samples each 1,248 programs · 3.6 h PATH A · ground truth (grading only) each candidate vs golden answer formal equivalence → correct / wrong much stronger than “passed the testbench” PATH B · the signal (deployable) candidate vs candidate, pairwise → 1 class or many never sees the golden answer does Path B predict Path A? ALL CORRECT ≥1 WRONG 1 class 44 3 >1 class 0 63 110 clean problems the 3 are semantic collapse: all agree, all wrong Then: does a cheap heuristic do the same job? tuned to the same operating point (never raise a false alarm), then measure recall formal partition 95.5% spec length 7.6% text similarity / code length 0.0% AUROC 0.977 formal 0.877 best heuristic Δ=0.100, p=0.001

Method note. The outcome variable is ground truth from the golden references, never the predictor. One half of the formal signal is analytic rather than empirical: if the samples fall into more than one class, at least one is wrong by construction. The empirical content is therefore the other half, the 44/47 figure, and the recall comparison against baselines. AUROC differences are paired bootstrap, 4,000 resamples.

Headline evidence

Everything measured, nothing asserted

95.5%problems containing a wrong implementation, caught at zero false alarms
7.6%best cheap heuristic at the same operating point
0.977AUROC vs 0.877 for the best heuristic (Δ=0.100, p=0.001)
93.6%when the k answers agree, all k are correct (44 of 47)
6.4%semantic collapse: agree but all wrong (3 of 47)
4 / 7ResBench modules where testbench-passing code is provably non-equivalent

Evidence explorer

The actual data

Unresolved and excluded rows are rendered inert and are excluded from every reported statistic, in both directions.

Specimens

What the solver actually found

Each verdict comes with a machine-derived witness, hand-checkable in under a minute.

1 · A benchmark certifying a real logic bug

air_quality_index · ResBench · both implementations passed the official testbench · solver proves they are different functions

Signal Name             Dec       Hex           Bin
\in_no2                 251        fb      11111011
\in_pm10                255        ff      11111111
\in_pm2_5               254        fe      11111110
SAT proof finished - model found: FAIL!
correct · min = 251
assign min_val =
  (pm2_5 <= pm10)
    ? ((pm2_5 <= no2) ? pm2_5 : no2)
    : ((pm10  <= no2) ? pm10  : no2);
wrong · min = 254
end else begin        // pm2_5 < pm10
  if (pm10 >= no2) begin
    max_val = pm10;
    min_val = pm2_5;  // never compares no2
  end

Outputs 355 instead of 354. The official testbench applies 3 input vectors over a 24-bit (16.7 million point) input space, and its test cases are numbered 3, 4 and 5: cases 1 and 2 do not exist in the file.

2 · Nine commercial models, one shared misconception

relu · ResBench · 22 of 23 compiling failures across GPT-4, GPT-4o, o1-mini, Llama-3.1-405B, qwen-max, qwen-plus, qwen2.5-coder-32B, Codestral and GPT-3.5 compute the identical wrong function

fails · 95.7% share
assign out = (in_0 > 16'd0) ? in_0 : 16'd0;
passes
assign out = (in_0 > 0) ? in_0 : 0;

Unsigned literal forces an unsigned comparison, so the function is identity on all negative inputs. The specification is one sentence, “Implement a Verilog module to compute the ReLU activation function,” and never constrains signedness. The counterexample localises the defect to a single missing specification constraint. That is the input to the causal experiment.

3 · Semantic collapse: all eight agree, all eight wrong

Prob089_ece241_2014_q5a · VerilogEval · spec asks for a serial machine processing bits as they arrive, for numbers of arbitrary length

all 8 samples
reg [31:0] shift_reg;
...
shift_reg <= {shift_reg[31:1], x};
...
assign z = output_valid
  ? ~shift_reg + 1 : 32'b0;
// 32-bit expression → 1-bit port
// fixed 32 bits, not arbitrary length
golden reference
parameter A=0,B=1,C=2;
reg [1:0] state;
always @(posedge clk, posedge areset)
  if (areset) state <= A;
  else case (state)
    A: state <= x ? C : A;
    B: state <= x ? B : C;
    C: state <= x ? B : C;
  endcase
assign z = (state == C);

Every sample buffered the number then negated it, instead of streaming. Eight independent attempts, one coherent misconception. This is the method's honest failure mode: agreement is good news, not proof. It happens on 6.4% of agreement cases here, comparable to software (3% HumanEval, over 10% MBPP, per Richter & Papadakis).

4 · Why text similarity is the wrong instrument

Prob006_vectorr · spec: “reverse the bit ordering of the input port”

assign out = {in[7], in[6], in[5], in[4], in[3], in[2], in[1], in[0]};

Descending concatenation reconstructs the operand, so this is the identity. Five of eight samples emitted it. Conversely, on Prob009_popcount3 an addition chain, a bare sum and an eight-line case table were proved to be one circuit. Median textual diversity was 7 distinct programs out of 8 in correct and incorrect cases alike, so surface similarity carries no signal in either direction.

Positioning

How this differs from the nearest work

Two papers from Schlichtmann's group at TU München do something adjacent. Both PDFs are in salvage/papers/. I read both in full; the quotes below are verbatim.

WorkWhat it doesHow it decides two candidates behave the sameWhy ours is different
VRank
ISQED 2025
arXiv:2502.00028		 Generates candidates, clusters them, ranks clusters, picks the best. Reports +10.5% pass@1 on VerilogEval-Human. “we group Verilog code candidates into clusters based on identical outputs when tested against the same testbench, which is also generated by LLMs” Their rule is provably blind on the cases that matter: two candidates that both pass necessarily agree on every test case, so they always land in the same cluster. Measured gap: 4 of 7 ResBench modules where all passing implementations look identical to a testbench and are provably different circuits. Also: theirs is a generation method aimed at raising pass rate; ours is a verification signal aimed at telling the engineer when to stop.
VClare
25 Jul 2026
arXiv:2607.24854		 Repairs imperfect specifications. Builds VerilogEval-Defect (156 tasks) by injecting spec defects. Reports +12.7%. “ci and cj belong to the same cluster if and only if their outputs match on all test cases”. Searched the full text for formal, SAT, Yosys, miter, model checking, BMC: none appear.
RealBench
arXiv:2507.16200		 IP-level benchmark with 100% line-coverage testbenches and a formal checker. “44.2% of the Verilog code generated by GPT-4-Turbo, which passes the testbenches in RTLLMV2, fails in formal verification” They check candidate against a golden reference. We check candidates against each other, which needs no reference and therefore works in deployment, where no reference exists. Their number is our motivation, not our competition.

The unclaimed gap: candidate-versus-candidate formal partitioning of LLM RTL samples, used as a reference-free correctness signal and as a root-cause diagnostic. Searches for prior work on this returned nothing on point; that is an absence of evidence, and I would want one more pass before writing the related-work section.

Plan

Milestones to 20 September

Every week has a gate that can stop the project. The week-1 gate is the one that decides whether there is a paper.

Week
Dates
Deliverable
Gate
0 · done
to 3 Aug
Instrument built and validated. 17/17 self-test, 110 problems scored, all cheap baselines beaten with a significant margin.
passed
1
4–10 Aug
The causal experiment. Take failing cases, add the one missing specification sentence the counterexample points at, regenerate, measure Δpass. Placebo row: reword without adding information.
Δpass significant and placebo null. If the placebo moves, stop. ~2 min per case.
1
parallel
Memory-circuit coverage. Recover the 26 sequential problems excluded for having no reset, using a zero-init start-state contract.
Reference must be equivalent to itself. ~20 min to check.
2
11–17 Aug
Scale. Three local models on VerilogEval and RTLLM. Plus the ResBench nine-commercial-model condition, which is free because the 7,560 labelled generations already exist.
Effect must hold across models, not just qwen-7b.
3
18–24 Aug
k-sweep, calibration, contamination audit. How small can k be? Computed from data already on disk, no new generation.
If k=3 suffices, the cost objection disappears.
4–5
25 Aug – 7 Sep
Write. Related work from zero. Artifact release: corpus, scripts, per-problem outcomes, reproducible by one command.
Complete draft.
6
8–13 Sep
Abstract deadline 13 Sep.
no gate
6.5
14–20 Sep
Buffer. Full paper deadline 20 Sep AoE, firm.
no gate

Cut order if behind: drop RTLLM, then the third model, then calibration. Never cut the causal experiment or the placebo row. Without the placebo there is no causal claim and the paper reduces to a correlation, which is exactly what sank the last submission.

Risks

What is weakest, stated first

coverage
39 of 156 problems excluded (25%). 26 are sequential circuits with no reset, 6 have references that will not elaborate, 4 had no sample compile with matching ports, 3 failed the flow's own self-check. This is the first thing a reviewer will attack, and it is week-1 work.
contamination
VerilogEval derives from HDLBits, whose solutions sit in dozens of public GitHub repositories. The model has very likely seen these. This inflates the all-correct cases. It does not affect the formal-versus-heuristic comparison, since both were measured on the same data.
one model
The VerilogEval half is a single 7B model. The ResBench half covers nine commercial models, but not this specific experiment. Week 2 fixes this.
causality
Not yet proven. We can name the missing specification fact; we have not yet shown that restoring it repairs the output. That is the week-1 gate.
novelty
A reviewer may read this as VRank with a different tool. The defence is the degeneracy result plus a measured count of cases where testbench clustering and formal clustering disagree. Four is not enough; we need that at VerilogEval scale.

Reproduce

Everything is on disk

salvage/equivalence_clustering/
ec_v2.py, the formal flow, 1,093 lines, five start-state contracts with measured reflexivity. python3 ec_v2.py --self-test → 17/17.
salvage/formal_experiments/
generation, analysis, baseline and collapse scripts, plus ve_gen.json (1,248 generations) and all result files.
salvage/papers/
VRank, VClare, RealBench and the semantic-collapse paper as PDFs.
tooling
yosys only. No iverilog, no GPU, no API key, no paid service.

All figures on this page were produced by scripts run on a MacBook Air (M4, 16 GB) between 30 July and 3 August 2026. Numbers described as measured were re-run and reproduced independently; numbers read from published papers are quoted verbatim with their arXiv identifiers. Unresolved solver results are reported as unresolved and are never counted as evidence.