arXiv cs.AI· Wenji Fang, Yuchao Wu, Jing Wang, Zhiyao Xie·· 10 小时前AI 评分31
智能体 AI 遇上形式化验证：面向智能体硬件开发时代
Agentic AI Meets Formal Verification in the Era of Agentic Hardware Development
AI 导读
一篇 ASP-DAC'27 受邀论文综述了 AI 时代硬件形式化验证的方法与应用。文章从规格、证明构造和推理引擎三个层面分析智能体 AI 如何推进硬件形式化方法，并讨论形式化方法如何通过 RTL 生成、调试和保持正确性的优化来支撑可靠的 AI 驱动硬件开发。文章还展望了形式化推理成为自主硬件设计固有组成部分的“证明原生”硬件开发方向。
正文 · 原文
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