智能体 AI 与形式化验证相遇：智能体硬件开发时代的形式化方法综述
Agentic AI Meets Formal Verification in the Era of Agentic Hardware Development
AI 导读
这是一篇 ASP-DAC'27 邀请综述论文，概述 AI 时代硬件形式化方法的应用。文章分析智能体 AI 如何从规格、证明构建、推理引擎三个层面推进硬件形式化方法，并讨论形式化方法如何通过 RTL 生成、调试和保持正确性的优化支撑可靠的 AI 驱动硬件开发，最后展望形式化推理成为自主硬件设计固有部分的 proof-native 硬件开发方向。
正文 · 原文
Abstract:As AI agents become increasingly capable of generating and optimizing hardware circuits, ensuring the correctness of AI-generated designs becomes more important. Meanwhile, advances in AI lower the barriers to developing and applying formal methods, creating new opportunities to automate and improve hardware verification. This invited paper presents an overview of the methodologies and applications of hardware formal methods in the AI era. First, we examine how agentic AI advances hardware formal methods across three levels: specification, proof construction, and reasoning engines. Second, we discuss how formal methods support reliable AI-driven hardware development through RTL generation, debugging, and correctness-preserving optimization. We review representative research alongside our recent contributions, highlighting key technical advances and insights from experimental results. Finally, we discuss future research opportunities toward proof-native hardware development, where formal reasoning could become an integral part of autonomous hardware design.
| Comments: | ASP-DAC'27 Invited Paper |
| Subjects: | Artificial Intelligence (cs.AI); Hardware Architecture (cs.AR) |
| Cite as: | arXiv:2611.13705 [cs.AI] |
| (or arXiv:2611.13705v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2611.13705 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Wenji Fang [view email]
[v1]
Tue, 10 Nov 2026 07:57:20 UTC (7,242 KB)
来源：arXiv cs.AI · arxiv.org