cs.AR提交于 2026-10-09已译

面向 LLM 辅助硬件设计验证的综述

A Survey on LLM-Integrated Hardware Design Verification

Hao Zheng · Jaime Rafael Imperial · Bardia Nadimi · Xiangfei Kong

中文摘要

大语言模型(LLMs)正越来越多地集成到硬件验证流程中,用于自动化规约解读、验证工件生成、调试、形式化推理,以及工具编排。本综述系统回顾了 LLM 辅助的硬件功能验证研究,涵盖 SystemVerilog 断言生成、激励与测试平台生成、缺陷定位与设计修复、模型检查与等价性检查、SAT/SMT(布尔可满足性/可满足性模理论)求解优化,以及新兴的智能体驱动验证工作流。沿方法论、验证目标、工具交互、基准测试与评估准则对现有文献进行梳理,同时考察推理时技术(包括提示工程、检索增强、结构化推理与智能体工作流)与训练时适配方法。各研究方向呈现出共同模式:LLM 作为语义推理、搜索与编排组件嵌入到验证感知的工作流中效果最佳,而仿真器、形式化引擎、覆盖率工具与求解器提供可执行反馈与正确性证据。然而,工具被接受并不等同于验证正确,因为断言、测试、修复或证明可能通过既有检查,却未完整覆盖设计意图。由此,核心挑战在于规约与验证证据之间的语义对齐、与确定性工具的可扩展集成、对未见设计的泛化能力,以及对正确性、成本、鲁棒性与人力的严格评估。最后讨论向以规约为中心、神经-符号融合、持续运行的智能体验证系统等新兴方向,使 LLM 的灵活性与独立可校验的验证证据相结合。

关键要点

01问题:LLM 生成或修复的断言、测试与证明可能通过既有检查,却未忠实覆盖完整设计意图,工具接受不等于验证正确
02方法:按方法论、验证目标、工具交互、基准与评估准则梳理 LLM 在 SystemVerilog 断言、激励生成、缺陷定位、模型检查、SAT/SMT 优化及智能体工作流中的应用,区分推理时技术与训练时适配
03方法:LLM 在验证流程中扮演语义推理、搜索与编排角色,仿真器、形式化引擎、覆盖率工具与求解器负责提供可执行反馈和正确性证据
04结果:核心挑战为规约与验证证据的语义对齐、与确定性工具的可扩展集成、对未见设计的泛化,以及对正确性、成本、鲁棒性与人力成本的严格评估
05方向:面向以规约为中心、神经-符号融合、持续运行的智能体验证系统,将 LLM 灵活性与独立可校验证据相结合

解读

尚无解读。

原始英文摘要

arXiv:2610.10580v1 Announce Type: cross Abstract: 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.