Testbench Acceptance Is Not Equivalence: Formal Counterexamples for RTLLM and VerilogEval

RTLLM and VerilogEval score a Verilog design by running a fixed testbench. We check whether testbench acceptance implies functional equivalence to the reference design. For each design we use unbounded formal equivalence checking (temporal induction), and we re-simulate every counterexample in Icarus Verilog. RTLLM v2.1, single-edit mutants of the reference. Of the 43 designs we could evaluate, 12 (8 of them purely combinational) have a testbench that accepts a mutant which differs from the reference. In each of these 12, the difference shows up as concrete 0/1 output values even when registers start unknown (X). Each of the 4 sequential designs is clocked through reset before the step where they differ. Under the weaker convention that registers start at zero, the count is 21 of 43 (48.8%, 95% CI 33.3–64.5). Proven counterexamples account for 0.0–1.5 pp of the gap. The rest comes from samples the formal check could not certify. Model-generated candidates (VerilogEval v1-Human, four 7B models, n = 20). Certified pass@1 is 2.3–5.0 percentage points below testbench pass@1. These figures use each metric's best sampling temperature; within a single temperature the gap reaches 5.35 pp. The model ranking is unchanged. This record is part of a series of grader-soundness audits; each releases replayable counterexamples in the same passport format. Release. 127 counterexample cases ("passports") that we replayed in Icarus with a reset pulse added at the start, and on which the reference and candidate still differ (113 RTLLM, 14 VerilogEval). Each passport ships with its replay testbench. We also release the list of RTLLM mutants that survive the testbench.