Agentic AI-based Coverage Closure for Formal Verification

Sivaram Pothireddypalli; Ashish Raman; Deepak Narayan Gadde; Aman Kumar

cs.AIMar 3, 2026

Agentic AI-based Coverage Closure for Formal Verification

Authors: Sivaram Pothireddypalli, Ashish Raman, Deepak Narayan Gadde, Aman Kumar

Organizations: Infineon Technologies India Private Limited, India · Dr. B R Ambedkar National Institute of Technology Jalandhar, India · Infineon Technologies Dresden AG & Co. KG, Germany

Abstract

Coverage closure is a critical requirement in Integrated Chip (IC) development process and key metric for verification sign-off. However, traditional exhaustive approaches often fail to achieve full coverage within project timelines. This study presents an agentic AI-driven workflow that utilizes Large Language Model (LLM)-enabled Generative AI (GenAI) to automate coverage analysis for formal verification, identify coverage gaps, and generate the required formal properties. The framework accelerates verification efficiency by systematically addressing coverage holes. Benchmarking open-source and internal designs reveals a measurable increase in coverage metrics, with improvements correlated to the complexity of the design. Comparative analysis validates the effectiveness of this approach. These results highlight the potential of agentic AI-based techniques to improve formal verification productivity and support comprehensive coverage closure.

Figures & tables

Figure 1: Agentic AI methodology for formal verification [ 9 ]

Figure 2: Depiction of agentic AI performing workflow execution [ 7 ]

Figure 3: Basic flow diagram of coverage pipeline

Figure 4: Overview of the coverage agent workflow

Design	Metric	Without coverage agents			With coverage agents
Design	Metric	GPT-4.1	GPT-5	Llama3.3	GPT-4.1	GPT-5	Llama3.3
ECC	# Properties	40	23	15	110	35	41
	Proven (%)	90	95.65	73.33	83.36	80	60.97
	Coverage (%)	61.72	70.30	70.71	89.30	92.11	89.60
CIC Decimator [ 15 ]	# Properties	13	28	10	28	33	17
	Proven (%)	61.5	53.57	50	82.14	78.78	52.94

Table I : Saarthi performance across designs with coverage agents

Panel of Figure 5 — Figure 5: Coverage metrics comparison across various designs using different models

Explore similar work

Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification
Mar 3, 2026Aman Kumar, Deepak Narayan Gadde, Luu Danh Minh +3LLM Agent Verification Formal Hardware Verification
Infineon Technologies India Private Limited, India · Infineon Technologies Dresden AG & Co. KG, Germany · Infineon Technologies Vietnam Company Ltd., Vietnam
UCAgent: An End-to-End Agent for Block-Level Functional Verification
Mar 26, 2026Junyue Wang, Zhicheng Yao, Yan Pi +6LLM Agent Verification Automated Test Generation
State Key Lab of Processors, Institute of Computing Technology, CAS · University of Chinese Academy of Sciences · Beijing Institute of Open Source Chip
LLM4Cov: Execution-Aware Agentic Learning for High-coverage Testbench Generation
Feb 18, 2026Hejia Zhang, Zhongming Yu, Chia-Tung Ho +3LLM Agent Training Automated Test Generation
University of California San Diego, USA · NVIDIA · Agentrys

Mar 3, 2026J/K move · Enter open · S save

Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification

Aman Kumar, Deepak Narayan Gadde, Luu Danh Minh, Vaisakh Naduvodi Viswambharan+2

Infineon Technologies India Private Limited, India · Infineon Technologies Dresden AG & Co. KG, Germany · Infineon Technologies Vietnam Company Ltd., Vietnam

LLM Agent Verification Formal Hardware Verification AI Agent Reliability Agentic RAG

Open paper AskPDF arXiv

Saarthi is an agentic AI framework that uses multi-agent collaboration to perform end-to-end formal verification. Even though the framework provides a complete flow from specification to coverage closure, with around 40% efficacy, there are several challenges that need to be addressed to make it more robust and reliable. Artificial General Intelligence (AGI) is still a distant goal, and current Large Language Model (LLM)-based agents are prone to hallucinations and making mistakes, especially when dealing with complex tasks such as formal verification. However, with the right enhancements and improvements, we believe that Saarthi can be a significant step towards achieving domain-specific general intelligence for formal verification. Especially for problems that require Short Term, Short Context (STSC) capabilities, such as formal verification, Saarthi can be a powerful tool to assist verification engineers in their work. In this paper, we present two key enhancements to the Saarthi framework: (1) a structured rulebook and specification grammar to improve the accuracy and controllability of SystemVerilog Assertion (SVA) generation, and (2) integration of advanced Retrieval Augmented Generation (RAG) techniques, such as GraphRAG, to provide agents with access to technical knowledge and best practices for iterative refinement and improvement of outputs. We also benchmark these enhancements for the overall Saarthi framework using challenging test cases from NVIDIA's CVDP benchmark targeting formal verification. Our benchmark results stand out with a 70% improvement in the accuracy of generated assertions, and a 50% reduction in the number of iterations required to achieve coverage closure.

Abstract

Explore similar work

Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification

UCAgent: An End-to-End Agent for Block-Level Functional Verification

LLM4Cov: Execution-Aware Agentic Learning for High-coverage Testbench Generation