用大模型生成硬件验证断言，构建了首个层次化验证数据集与评估体系。
HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification
- 设计全流程工具链，结合大模型与RTL预处理自动生成系统验证断言。
- 在342个模块上生成断言，检出70.2%的注入缺陷，但误报率高达40%。
- 提出六维评估标准，揭示大模型断言存在覆盖不足和虚真问题。
我们提出HierSVA，一个集成流水线、数据集与基准的框架，用于大模型驱动的分层硬件形式化验证。HierSVA-SP将RTL预处理工具链与大模型参与的验证流程结合，生成分层RTL的参考SystemVerilog断言。应用于BaseJump STL得到HierSVA-DS，包含342个模块，层次深度0–9，附带28个含自然语言说明和变种的模块-漏洞对。HierSVA-B将断言质量分解为六个维度：语法正确性、证明成功率、虚真性、规范忠实度、变异覆盖率与形式核心覆盖率。对12个近期大模型的评估显示：模块级编译率为67.1%；可验证断言中82.1%非虚真，但仅检测到70.2%的可检测缺陷，形式核心覆盖仅36.2%。在深子集211个模型-模块组合中，断言对错误RTL召回率达0.87，但40%预测为错的实则正确，精确率仅为0.60。代理模式提升S1类可证明性与强度，但性能增长趋缓并波动。代码与资源见GitHub及HuggingFace。
原文摘要 · Abstract (English)
We present HierSVA, an integrated suite that combines a pipeline, dataset, and benchmark for LLM-driven hierarchical hardware formal verification. HierSVA-SP pairs an RTL preprocessing toolchain with an LLM-in-the-loop formal verification flow to produce reference SystemVerilog Assertions (SVA) on hierarchical RTL. Applying it to BaseJump STL yields HierSVA-DS, a dataset of 342 modules, with hierarchy metadata and depths 0--9, accompanied by a deep subset of 28 module-bug pairs with natural-language specifications and bug variants. HierSVA-B decomposes assertion quality into six metric axes: syntax correctness, assertion proof success rate, vacuity, specification faithfulness, mutation coverage, and formal core coverage. Applying HierSVA-B to twelve recent LLMs reveals three findings. First, the module-level compile rate is 67.1\%; among generated assertions in evaluable runs, 82.1\% prove non-vacuously, but the corresponding assertion sets detect only 70.2\% of eligible injected faults and cover 36.2\% of the formal core. Second, on 211 evaluable model--module entries in the deep subset, assertion sets flag buggy RTL with 0.87 recall, but 40\% of predicted-buggy outcomes are false positives on correct RTL, limiting precision to 0.60. Third, agentic mode improves S1-style provability and strength metrics, but gains plateau and oscillate. Codes and artifacts are available at \href{https://github.com/HierSVAAnon/HierSVACodeAndArtifacts}{https://github.com/HierSVAAnon/HierSVACodeAndArtifacts}. Dataset is available at \href{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。