arXiv:2605.27472cs.ARcs.AI2026-05

用真实硬件设计数据集,测试大模型生成验证断言的能力

AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications

论文配图:AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications
图 1 · 摘自论文原文
  • 基于83个真实电路设计构建评测基准
  • 支持预防错误和发现漏洞两种实际场景
  • 首次用带错的RTL代码评估检测效果

断言式验证(ABV)是现代硬件设计的核心,但将设计意图转化为正式的SystemVerilog断言(SVAs)仍依赖人工,耗时且易出错。尽管大语言模型(LLMs)在自动化该过程方面展现潜力,现有评测基准受限于不切实际的任务设定、弱化规格输入和简化评估方式。为此,我们提出AssertLLM2——一个开源的硬件验证断言生成评测基准。该基准包含83个真实世界的设计,覆盖13类功能模块,每个设计均提供结构化规格说明、经验证的依赖完整黄金RTL及系统性变异的带错RTL版本。支持两种实用场景:在缺陷预防场景中,从规格生成断言以防范设计错误;在缺陷挖掘场景中,生成断言以暴露预期行为与故障实现间的差异。据我们所知,AssertLLM2是首个明确以带错RTL为输入来评估漏洞检测能力的基准。其采用更严格的评估框架,涵盖语法正确性、形式可证明性、覆盖率和基于变异的漏洞检测。该基准推动了断言生成的现实评估,并为先进LLMs在实际硬件验证中的表现建立了严谨基线。

原文摘要 · Abstract (English)

Assertion-based verification (ABV) is a cornerstone of modern hardware design, yet manually translating design intent into formal SystemVerilog Assertions (SVAs) remains labor-intensive and error-prone. While Large Language Models (LLMs) show promise for automating this process, existing benchmarks remain limited by unrealistic task formulations, weak specification inputs, and oversimplified evaluation. To address these limitations, we introduce AssertLLM2, an open-source benchmark for realistic assertion generation in hardware verification. AssertLLM2 contains 83 real-world designs across 13 functional categories. For each design, the benchmark provides a structured design specification, a verified dependency-complete golden RTL, and systematically mutated buggy RTL variants. These support two practical settings: bug-prevention, where assertions are generated from specifications to guard against design errors, and bug-hunting, where assertions are generated to expose discrepancies between intended behavior and faulty implementations. To the best of our knowledge, AssertLLM2 is the first benchmark to explicitly use buggy RTL as input to evaluate bug-detection capability. AssertLLM2 further adopts a more rigorous evaluation framework spanning syntactic validity, formal provability, coverage, and mutation-based bug detection. Our benchmark enables a more realistic and extensive assessment of assertion generation and establishes rigorous baselines for state-of-the-art LLMs in practical hardware verification.

硬件验证大模型断言生成评测基准

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。