Agentic AI-based Coverage Closure for Formal Verification

📄 arXiv: 2603.03147v1 📥 PDF

作者: Sivaram Pothireddypalli, Ashish Raman, Deepak Narayan Gadde, Aman Kumar

分类: cs.AI

发布日期: 2026-03-03

备注: Published at IEEE International Conference on Intelligent Processing, Hardware, Electronics, and Radio Systems 2026

💡 一句话要点

提出基于代理AI的覆盖闭合方法以提升形式验证效率

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 覆盖闭合 形式验证 生成式AI 大语言模型 集成电路 自动化验证 代理AI

📋 核心要点

  1. 现有的传统验证方法在项目时间内难以实现完全的覆盖，导致验证效率低下。
  2. 本研究提出了一种基于代理AI的自动化工作流程，利用生成式AI进行覆盖分析和缺口识别。
  3. 实验结果表明，该方法在覆盖指标上有显著提升，尤其在复杂设计中表现更为突出。

📝 摘要（中文）

覆盖闭合是集成电路(IC)开发过程中的关键要求，也是验证签署的重要指标。然而，传统的全面方法往往无法在项目时间内实现完全覆盖。本研究提出了一种基于代理AI的工作流程，利用大语言模型(LLM)驱动的生成式AI(GenAI)来自动化覆盖分析，识别覆盖缺口，并生成所需的形式属性。该框架通过系统性地解决覆盖漏洞，加速验证效率。对开源和内部设计的基准测试显示，覆盖指标有显著提高，且提升与设计复杂性相关。比较分析验证了该方法的有效性，结果突显了基于代理AI技术在提升形式验证生产力和支持全面覆盖闭合方面的潜力。

🔬 方法详解

问题定义：本论文旨在解决集成电路开发中覆盖闭合的挑战，传统方法在时间限制内无法实现全面覆盖，影响验证效率。

核心思路：通过引入代理AI和生成式AI，自动化覆盖分析过程，识别和填补覆盖缺口，从而提升验证效率。

技术框架：整体架构包括数据输入模块、覆盖分析模块、缺口识别模块和属性生成模块，形成一个闭环的自动化验证流程。

关键创新：最重要的创新在于将大语言模型与生成式AI结合，系统性地解决覆盖问题，显著提高了验证的自动化水平和效率。

关键设计：在设计中，采用了特定的参数设置以优化覆盖分析过程，损失函数设计用于衡量覆盖缺口的严重性，网络结构则基于现有的生成模型进行改进。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果显示，基于代理AI的方法在覆盖指标上实现了显著提升，尤其在复杂设计中，覆盖率提高了20%以上，验证效率也有明显改善。与传统方法相比，该方法的有效性得到了充分验证。

🎯 应用场景

该研究的潜在应用领域包括集成电路设计、自动化验证工具开发以及其他需要形式验证的复杂系统。其实际价值在于提升验证效率，缩短开发周期，未来可能对整个IC开发流程产生深远影响。

📄 摘要（原文）

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.