用AI自动发现芯片验证中的覆盖率漏洞并生成修复代码
Agentic AI-based Coverage Closure for Formal Verification
- 用大模型驱动的智能体自动分析验证覆盖率
- 实测提升覆盖率，复杂设计改进更明显
- 适合芯片验证工程师快速闭环验证流程
覆盖率闭合是集成电路开发中关键的验证要求，也是验证签核的核心指标。然而，传统穷举方法常无法在项目周期内达成全覆盖。本文提出一种基于智能体AI的自动化工作流，利用大语言模型驱动的生成式AI（GenAI）自动完成形式验证的覆盖率分析，识别覆盖率缺口，并生成所需的形式化属性。该框架通过系统性填补覆盖率盲区，显著提升验证效率。对开源及内部设计的基准测试显示，覆盖率指标均有可测量提升，且改进程度与设计复杂度正相关。对比分析进一步验证了该方法的有效性。结果表明，基于智能体的AI技术具有提升形式验证生产率、实现全面覆盖率闭合的巨大潜力。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。