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.

翻译：基于断言的验证是现代硬件设计的基石，但将设计意图手动转化为形式化SystemVerilog断言仍存在劳动强度高且易出错的问题。尽管大语言模型在自动化该流程方面展现出潜力，现有基准测试仍受限于不切实际的任务设定、弱规格输入及过度简化的评估。为应对这些局限，我们提出开源基准测试AssertLLM2，用于真实场景下硬件验证的断言生成。该基准包含13个功能类别的83个真实设计，为每个设计提供结构化设计规格、经验证依赖关系完备的黄金级RTL代码及系统性变异的带缺陷RTL变体。这些资源支持两种实际场景：缺陷预防（根据规格生成断言以防范设计错误）与缺陷追踪（生成断言以暴露预期行为与错误实现间的差异）。据我们所知，AssertLLM2是首个明确使用带缺陷RTL作为输入以评估缺陷检测能力的基准测试。该基准进一步采用更严格的评估框架，涵盖语法有效性、形式化可证明性、覆盖率及基于变异的缺陷检测。我们的基准测试能够对断言生成进行更真实全面的评估，并为实际硬件验证中的先进大语言模型建立严苛基线。