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

arXiv: https://arxiv.org/abs/2605.27472 · HTML: https://mlsanity.com/paper/2605.27472/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 32 references that are in the map.
- First posted on arXiv 26 May 2026.

## Builds on (most cited first, 11 of 11)

- [Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities](https://mlsanity.com/paper/2507.06261/) (2025)
- [OpenAI GPT-5 System Card](https://mlsanity.com/paper/2601.03267/) (2025)
- [DeepSeek-V3.2: Pushing the Frontier of Open Large Language Models](https://mlsanity.com/paper/2512.02556/) (2025)
- [Qwen3-Coder-Next Technical Report](https://mlsanity.com/paper/2603.00729/) (2026)
- [AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2402.00386/) (2024)
- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)
- [FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware](https://mlsanity.com/paper/2410.23299/) (2024)
- [Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Dataset](https://mlsanity.com/paper/2503.08923/) (2025)
- [AssertGen: Enhancement of LLM-aided Assertion Generation through Cross-Layer Signal Bridging](https://mlsanity.com/paper/2509.23674/) (2025)
- [AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction](https://mlsanity.com/paper/2507.10338/) (2025)
- [AssertMiner: Module-Level Spec Generation and Assertion Mining using Static Analysis Guided LLMs](https://mlsanity.com/paper/2511.10007/) (2025)

## Built on by (most cited first, 3 of 3)

- [EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations](https://mlsanity.com/paper/2609.26751/) (2026)
- [SpecRead: A Benchmark for Measuring Whether Language Models Understand Hardware Specifications](https://mlsanity.com/paper/2609.33699/) (2026)
- [A Survey on LLM-Integrated Hardware Design Verification](https://mlsanity.com/paper/2610.10580/) (2026)

## Abstract (arXiv)

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.
