- First-silicon success just hit 14% — the lowest in 20 years of tracking. It was 32% in 2020. And now your team is shipping LLM-generated Verilog. The bug classes an LLM introduces are exactly the ones that survive simulation and kill the tape-out. 🧵
- A 5nm mask set is $10M. At 3nm it pushes $40M. A respin adds a 3–6 month slip — and on an 18-month product cycle, six months gone can erase half of lifetime revenue. Verification isn't a cost center. It's insurance against a $10M+ mistake.
- The part nobody says out loud: 70% of respins come from spec changes, not pure logic bugs (2024 Wilson/Siemens). So any "AI finds your bugs" pitch that only catches logic errors is addressing a fraction of what actually blows tape-outs.
- The LLM failure mode that should scare you isn't bad syntax — compilers catch that in seconds. It's vacuity. The LLM writes an SVA property. The formal engine proves it. You ship. The property was trivially true because its antecedent never fires.
- Now you hold a certificate that says "proven" on a broken design. That's worse than no verification. Siemens has warned about vacuous proofs since 2017, and flows still ship without vacuity checks. A formal sign-off that skips them is theater.
- Three more an LLM smuggles past simulation: blocking-for-nonblocking swaps; AXI/AHB violations buried on page 84 of the spec; CDC crossings with no synchronizer. Sim can't model metastability. Formal alone found 65+ bugs in one RISC-V core (Ibex) that simulation never hit.
- Vendor reality, said plainly: JasperGold and VC Formal are genuinely the gold standard. But JasperGold's historical baseline ($225K + $45K/seat) prices out most early-stage RISC-V and AI-accelerator shops. Three vendors now control ~85% of EDA.
- Meanwhile you're pitched at every DAC: ChipAgents ($74M raised), Normal Computing ($85M+, Samsung-backed), a half-dozen more "agentic EDA" startups. Most are cloud-first — dead on arrival with a fabless team that won't ship RTL off-prem. That's the opening nobody fills.
- The AlphaChip RL-placement story everyone cites? Markov's critique clocked it at 32.31 hrs vs 12.5 hrs for tuned simulated annealing — and 0.05 hrs for a commercial Cadence tool. Three years on, no independent replication. We'd rather tell you that than sell the hype.
- Our take: don't buy another tool. Wrap a fine-tuned open-weight model around the formal engine you already own — JasperGold, VC Formal, Questa, or SymbiYosys — on your own hardware. No RTL leaves your network. Vacuity and coverage metrics in front of every proof.
- If you're running LLMs on Verilog today, which class are you most exposed to — protocol, vacuity, or CDC? And does your formal sign-off actually check for vacuity, or just hand you a green proof? #RISCV #FormalVerification
- We wrote up the full HDL hallucination taxonomy, the honest vendor landscape, and on-prem deployment options here: https://veriprajna.com/solutions/semiconductor-ai-verification