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

2025/09/16 by Yunsheng Bai, Bai, Yunsheng, Ghaith Bany Hamad +7 · 2 citations
Computer Science · #Artificial Intelligence (cs.AI) #Embedded Systems Design Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Hardware Architecture (cs.AR) #VLSI and Analog Circuit Testing

paper · pdf · doi:10.48550/arxiv.2510.15906

openalex publication_date 2025/09/16 · openalex created_date 2025/10/22 · openalex updated_date 2026/07/28

Abstract

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.

Citations

• HLSDebugger: Identification and Correction of Logic Bugs in HLS Code with LLM Solutions
• SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Models
• Configured OpenTitan and FabScalar designs
• VeriDebug: A Unified LLM for Verilog Debugging via Contrastive Embedding and Guided Correction
• Insights from Rights and Wrongs: A Large Language Model for Solving Assertion Failures in RTL Design
• Saarthi: The First AI Formal Verification Engineer
• Generative AI Augmented Induction-based Formal Verification
• MEIC: Re-thinking RTL Debug Automation using LLMs
• Encouraging Divergent Thinking in Large Language Models through Multi-Agent Debate
• Tree of Thoughts: Deliberate Problem Solving with Large Language Models
• Teaching Large Language Models to Self-Debug
• Self-Refine: Iterative Refinement with Self-Feedback
• LEVER: Learning to Verify Language-to-Code Generation with Execution
• Affective Coherence Monitoring for Transformer-Based Language Models
• Self-Consistency Improves Chain of Thought Reasoning in Language Models
• Training Verifiers to Solve Math Word Problems
• AutoSVA: Democratizing Formal Verification of RTL Module Interactions

Cited by

• The Dawn of Agentic EDA: A Survey of Autonomous Digital Chip Design
• Learning to Debug: LLM-Organized Knowledge Trees for Solving RTL Assertion Failures

Related

• Towards LLM-based Root Cause Analysis of Hardware Design Failures
• Learning to Debug: LLM-Organized Knowledge Trees for Solving RTL Assertion Failures
• VeriBug: An Attention-based Framework for Bug-Localization in Hardware Designs
• FIXME: Towards End-to-End Benchmarking of LLM-Aided Design Verification
• BugGen: A Self-Correcting Multi-Agent LLM Pipeline for Realistic RTL Bug Synthesis