# FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures

arXiv: https://arxiv.org/abs/2510.15906 · HTML: https://mlsanity.com/paper/2510.15906/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 18 of its 33 references that are in the map.
- First posted on arXiv 16 Sep 2025.

## Builds on (most cited first, 18 of 18)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [Constitutional AI: Harmlessness from AI Feedback](https://mlsanity.com/paper/2212.08073/) (2022)
- [Encouraging Divergent Thinking in Large Language Models through Multi-Agent Debate](https://mlsanity.com/paper/2305.19118/) (2023)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [LEVER: Learning to Verify Language-to-Code Generation with Execution](https://mlsanity.com/paper/2302.08468/) (2023)
- [MEIC: Re-thinking RTL Debug Automation using LLMs](https://mlsanity.com/paper/2405.06840/) (2024)
- [LLM4SecHW: Leveraging Domain Specific Large Language Model for Hardware Debugging](https://mlsanity.com/paper/2401.16448/) (2024)
- [AutoSVA: Democratizing Formal Verification of RTL Module Interactions](https://mlsanity.com/paper/2104.04003/) (2021)
- [VeriDebug: A Unified LLM for Verilog Debugging via Contrastive Embedding and Guided Correction](https://mlsanity.com/paper/2504.19099/) (2025)
- [Saarthi: The First AI Formal Verification Engineer](https://mlsanity.com/paper/2502.16662/) (2025)
- [Insights from Rights and Wrongs: A Large Language Model for Solving Assertion Failures in RTL Design](https://mlsanity.com/paper/2503.04057/) (2025)
- [SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Models](https://mlsanity.com/paper/2506.20415/) (2025)
- [HLSDebugger: Identification and Correction of Logic Bugs in HLS Code with LLM Solutions](https://mlsanity.com/paper/2507.21485/) (2025)
- [Generative AI Augmented Induction-based Formal Verification](https://mlsanity.com/paper/2407.18965/) (2024)
- [VCDiag: Classifying Erroneous Waveforms for Failure Triage Acceleration](https://mlsanity.com/paper/2506.03590/) (2025)

## Built on by (most cited first, 5 of 5)

- [QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis](https://mlsanity.com/paper/2603.14239/) (2026)
- [Learning to Debug: LLM-Organized Knowledge Trees for Solving RTL Assertion Failures](https://mlsanity.com/paper/2511.17833/) (2025)
- [WaveformQA: Benchmarking LLM Temporal Reasoning on Digital Waveforms](https://mlsanity.com/paper/2607.20638/) (2026)
- [Can Agents Design Better Chips with a Higher Level Abstraction?](https://mlsanity.com/paper/2609.21157/) (2026)
- [A Survey on LLM-Integrated Hardware Design Verification](https://mlsanity.com/paper/2610.10580/) (2026)

## Abstract (arXiv)

Debugging formal verification (FV) failures represents one of the most time-consuming bottlenecks in modern hardware design workflows. When properties fail, engineers must manually trace through complex counter-examples spanning multiple cycles, analyze waveforms, and cross-reference design specifications to identify root causes - a process that can consume hours or days per bug. Existing solutions are largely limited to manual waveform viewers or simple automated tools that cannot reason about the complex interplay between design intent and implementation logic. We present FVDebug, an intelligent system that automates root-cause analysis by combining multiple data sources - waveforms, RTL code, design specifications - to transform failure traces into actionable insights. Our approach features a novel pipeline: (1) Causal Graph Synthesis that structures failure traces into directed acyclic graphs, (2) Graph Scanner using batched Large Language Model (LLM) analysis with for-and-against prompting to identify suspicious nodes, and (3) Insight Rover leveraging agentic narrative exploration to generate high-level causal explanations. FVDebug further provides concrete RTL fixes through its Fix Generator. Evaluated on open benchmarks, FVDebug attains high hypothesis quality and strong Pass@k fix rates. We further report results on two proprietary, production-scale FV counterexamples. These results demonstrate FVDebug's applicability from academic benchmarks to industrial designs.