First-silicon success hit 14% in 2024 — the lowest number in twenty years of the Wilson Research Group / Siemens EDA Functional Verification tracking study. In 2020 the figure was 32%. The decline is structural: design complexity has outpaced the verification tools, specification is mutating faster than the testbench can close it, and LLM-generated RTL has added a new class of failure that formal verification catches — but only when it's configured to look.
Most fabless design teams are now using LLMs somewhere in their RTL workflow. GitHub Copilot, domain-specific copilots from Cadence and Synopsys, and the six agentic AI startups that collectively backed by more than $160M in venture capital — ChipAgents ($74M total as of February 2026, with TSMC, Bessemer, Micron, and MediaTek as backers), Normal Computing ($85M+ total with Samsung Catalyst leading the March 2026 round), and MooresLabAI, Bronco AI, Silimate, and Axiomise in various configurations. The EDA vendors' consensus — shaped mostly by vendors selling the tools — is that LLMs accelerate design and that the risk is manageable. After studying the failure modes across both simulation and formal verification pipelines, our view is that the risk is specific, underestimated, and concentrated in the bug classes that bypass simulation entirely.
The Bug Class That Breaks Silicon After Formal Gives You a Certificate
The LLM+Verilog research literature has grown from six papers in 2023 to sixty-four in 2025. The benchmarks — VerilogEval, RTLLM v2, HaVen, VeriThoughts — now characterize how models fail, not just whether they do.
Code that doesn't compile is the failure mode LLM marketing focuses on. Verilator catches it in seconds. It is genuinely the least interesting class.
The cases that kill tapeouts arrive later in the stack. An LLM trained predominantly on Python and C writes Verilog as if statements execute sequentially — so it reaches for blocking assignments inside always_ff blocks where non-blocking is required. Depending on the simulator's event-scheduling order, this can masquerade as correct behavior during simulation, produce different logic in synthesis, and ship a 1-cycle bypass where the designer built a 2-cycle pipeline. No lint tool catches this by default.
AXI4 protocol violations follow a similar trajectory but surface even later. The generated code compiles. It passes 90% of directed tests. It fails the first time the design is connected to a third-party memory controller that exercises the WVALID/AWREADY handshake at a timing edge the testbench didn't cover. That constraint lives on page 84 of the AMBA spec. Most directed testbenches never exercise it.
CDC failures — clock domain crossing violations, missing double-flop synchronizers — are invisible to RTL simulation entirely. Simulation doesn't model metastability. Accellera opened a CDC/RDC/Glitch interoperability standard in 2024 specifically because the fragmentation across SpyGlass, Questa CDC, and Conformal CDC was breaking chiplet-boundary sign-off at scale. The standard is the field's acknowledgment that the problem is industry-wide.
The worst class is the one that makes it past formal verification with a PROVEN certificate. The LLM generates an SVA property — req |-> ##[1:$] gnt, say — and the formal engine proves it. What neither the model nor the sign-off report surfaces is that req is tied low by an upstream assume. The antecedent never fires. The solver has proven that "whenever req fires, gnt follows" is vacuously true in a system where req never fires — which proves nothing about the arbiter's actual behavior. Siemens has been documenting vacuous proof failures since 2017. Any formal flow that doesn't run vacuity checks is theater, but most SymbiYosys-only shops skip them because the tooling doesn't expose vacuity as cleanly as JasperGold's VACUOUS status column — and JasperGold starts at $225K base with $45K/seat.
The formal tool proved exactly what you asked it to prove. The ask was vacuously true.
What Formal Verification Catches — and the Limit It Doesn't Talk About
Formal verification finds bugs simulation misses, and the record at production scale is clear. The Axiomise formal team found 65+ bugs in the Ibex RISC-V core — including six in the debug unit alone — in a processor already deployed inside Google OpenTitan. Those bugs had survived directed simulation. Pre-verified SVA property libraries for AXI4, AHB, and TileLink catch the protocol violations that testbenches leave open. Metastability injection in CDC paths closes the gap on clock-domain crossings that RTL sim can't see.
What formal doesn't catch: spec drift. The 2024 Wilson study puts 70% of respins at the door of specification changes, not logic bugs. A verification flow that catches logic bugs addresses a necessary but not sufficient subset of the problem. The harder challenge — specification mutating faster than the assertion library can track it — requires properties generated from the spec itself, maintained in sync via the same pipeline that produces RTL.
A formal sign-off that runs vacuity checks on week-old properties while the spec has moved is not a sign-off. It's a dated receipt.
Our semiconductor verification work wraps fine-tuned open-weight models around the customer's existing formal engine — JasperGold, VC Formal, Questa Formal, or SymbiYosys — and runs entirely on their hardware. The LLM's role is spec-to-assertion translation and vacuity-check enforcement. The formal engine proves or disproves. No RTL leaves the network.
The Vendor Landscape a DV Lead Is Actually Navigating
JasperGold and VC Formal are the gold standards. This is not contested. Synopsys ($6.1B FY24 revenue) launched AgentEngineer in March 2026, claiming L4 agentic workflow and 2-5x productivity gains. Cadence ($4.6B FY24, $7.0B FY25 backlog) launched the ChipStack AI Super Agent in February 2026. Siemens EDA (~$2.5B, the publisher of the Wilson study) delivered the Questa One AI-enabled suite at DAC 2025. The $35B Synopsys-Ansys acquisition is complete, adding multiphysics to Synopsys's stack. The top four EDA vendors now control roughly 85-90% of EDA revenue. These are the tools entrenched in every large fabless shop, and they should be.
The gaps: opinionated vendor-neutral RTL review, on-prem LLM inference for IP-sensitive customers, and custom RISC-V IP verification at early-stage fabless economics. Historical JasperGold licensing put it out of reach for most Series A RISC-V teams. The six agentic AI startups pitching into this space all face the same wall — RTL is crown-jewel IP, and the customers who most need AI-assisted verification are the ones who cannot send Verilog to any cloud endpoint, regardless of vendor assurances about data isolation.
The practical deployment for IP-sensitive teams is on-prem inference: fine-tuned open-weight models (Llama 4, Qwen 2.5 Coder, DeepSeek Coder) running on the customer's own compute cluster, with local RAG over their Verilog corpus, spec history, and past bug database. For automotive customers, there's a second constraint. ISO 26262 ASIL C/D sign-off requires a full TCL2/TCL3 qualification kit for every EDA tool in the sign-off chain. Adding an AI assistance layer without wrapping a pre-qualified engine — JasperGold, VC Formal, Questa Formal — invalidates the qualification package. Every AI tooling decision in an automotive sign-off flow is also a qualification-chain decision.
On the AlphaChip Question
The research scope behind this page includes RL-based macro placement, a topic that warrants more honesty than most vendor presentations offer. The 2020 Google Nature paper claimed RL beat simulated annealing for macro placement in TPU designs. By 2023, Igor Markov (Synopsys) had published a line-by-line methodological critique: AlphaChip Circuit Training takes 32.31 hours on the benchmark; tuned SA takes 12.5 hours; the Cadence commercial tool takes 0.05 hours. DeepMind published a rebuttal in November 2024 ("That Chip Has Sailed," arXiv 2411.10053). Three years on, no independent external replication has confirmed the original performance claims.
Our position: RL placement at commodity ASIC nodes isn't a credible pitch against DSO.ai or Cadence Cerebrus. The vendors with the data advantage and compute win that benchmark. The niches where a custom RL-assisted approach makes sense are more specific: 3D-IC and chiplet thermal-aware floorplanning where the incumbents' tools are still catching up on UCIe multi-die structures, analog layout automation, and RISC-V IP optimization using OpenROAD where the customer controls the objective function. We tell customers what the Markov critique actually says before we talk about what RL can do.
What the 14% Number Means for the Next Tape-Out
A 5nm respin is $10-20M in masks. A 3nm respin approaches $40M. A 6-month schedule slip on an 18-month product cycle can erase roughly half of lifetime revenue before the product reaches the market. The bug classes responsible — vacuity failures, protocol violations, CDC races, semantic assignment errors — are characterized, documented, and catchable with the right verification architecture. They are also the classes most likely to be introduced by LLM-generated RTL and most likely to be missed by DV teams that adopted AI tooling without updating their formal sign-off checklist.
The verification community will work through this the same way it worked through the CDC problem two decades ago: the failure modes will accumulate across enough tapeouts that the field formalizes countermeasures, the EDA giants build them into their tools, and vacuity checking becomes a standard step the way SpyGlass CDC checking became standard. The question is how many mask sets get spent in the interim.
If you're rethinking where LLM-generated RTL fits into your formal sign-off gate, the architecture we've built around this problem is there to look at. We'd especially like to hear from teams navigating the organizational question — when two sources are generating SVA properties simultaneously, who owns the assertion library, and how does that ownership show up in the sign-off review? That's where we see the most variation across shops, and we don't have a single answer yet.