集成大语言模型（LLM）的硬件设计验证综述

中文摘要 AI 辅助

大语言模型（LLM）正越来越多地被集成到硬件验证中，以自动化规范解读、验证工件生成、调试、形式推理和工具编排。本综述系统回顾了LLM辅助的硬件功能验证，涵盖SystemVerilog断言生成、激励与测试平台生成、漏洞定位与设计修复、模型检查与等价性检查、SAT/SMT优化以及新兴的智能体验证工作流。我们按方法、验证目标、工具交互、基准和评估标准对文献进行组织，研究了推理时技术（包括提示、检索、结构化推理和智能体工作流）以及训练时适配。在这些领域中，一个共同模式显现：LLM作为嵌入验证感知工作流中的语义推理、搜索和编排组件最为有效，而模拟器、形式引擎、覆盖率工具和求解器则提供可执行反馈和正确性证据。然而，仅工具接受度并不能确立验证正确性，因为断言、测试、修复或证明可能满足可用检查却未忠实地捕获完整设计意图。因此，我们将规范与验证证据间的语义对齐、与确定性工具的可扩展集成、对未见设计的泛化以及对正确性、成本、鲁棒性和人力投入的严格评估确定为关键挑战。最后，我们讨论了以规范为中心、神经符号和持久智能体验证系统的新兴方向，这些系统结合了LLM的灵活性与可独立验证的正确性证据。

英文摘要

Large language models (LLMs) are increasingly being integrated into hardware verification to automate specification interpretation, verification-artifact generation, debugging, formal reasoning, and tool orchestration. This survey provides a systematic review of LLM-assisted hardware functional verification across SystemVerilog assertion generation, stimulus and testbench generation, bug localization and design repair, model checking and equivalence checking, SAT/SMT optimization, and emerging agentic verification workflows. We organize the literature by methodology, verification objective, tool interaction, benchmark, and evaluation criterion, and examine both inference-time techniques--including prompting, retrieval, structured reasoning, and agentic workflows--and training-time adaptation. Across these areas, a common pattern emerges: LLMs are most effective as semantic reasoning, search, and orchestration components embedded within verification-aware workflows, while simulators, formal engines, coverage tools, and solvers provide executable feedback and correctness evidence. However, tool acceptance alone does not establish verification correctness, since assertions, tests, repairs, or proofs may satisfy available checks without faithfully capturing the complete design intent. We therefore identify semantic alignment between specifications and verification evidence, scalable integration with deterministic tools, generalization to unseen designs, and rigorous evaluation of correctness, cost, robustness, and human effort as key challenges. Finally, we discuss emerging directions toward specification-centered, neuro-symbolic, and persistent agentic verification systems that combine LLM flexibility with independently checkable verification evidence.

发表机构

• University of South Florida（南佛罗里达大学）

机构由 AI 辅助整理，请以论文原文为准。