# AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation

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

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 54 references that are in the map.
- First posted on arXiv 26 Jun 2024.

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [VerilogEval: Evaluating Large Language Models for Verilog Code Generation](https://mlsanity.com/paper/2309.07544/) (2023)
- [A Comprehensive Capability Analysis of GPT-3 and GPT-3.5 Series Models](https://mlsanity.com/paper/2303.10420/) (2023)
- [(Security) Assertions by Large Language Models](https://mlsanity.com/paper/2306.14027/) (2023)
- [Using LLMs to Facilitate Formal Verification of RTL](https://mlsanity.com/paper/2309.09437/) (2023)
- [ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation](https://mlsanity.com/paper/2402.00093/) (2024)
- [Isadora: Automated Information Flow Property Generation for Hardware Designs](https://mlsanity.com/paper/2106.07449/) (2021)

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

- [A Survey of Circuit Foundation Model: Foundation AI Models for VLSI Circuit Design and EDA](https://mlsanity.com/paper/2504.03711/) (2025)
- [TuRTLe: A Unified Evaluation of LLMs for RTL Generation](https://mlsanity.com/paper/2504.01986/) (2025)
- [Revolution or Hype? Seeking the Limits of Large Models in Hardware Design](https://mlsanity.com/paper/2509.04905/) (2025)
- [Are LLMs Ready for Practical Adoption for Assertion Generation?](https://mlsanity.com/paper/2502.20633/) (2025)
- [SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Models](https://mlsanity.com/paper/2506.20415/) (2025)
- [Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA](https://mlsanity.com/paper/2506.21569/) (2025)
- [HardSecBench: Benchmarking the Security Awareness of LLMs for Hardware Code Generation](https://mlsanity.com/paper/2601.13864/) (2026)
- [ContractEval: A Benchmark for Evaluating Contract-Satisfying Assertions in Code Generation](https://mlsanity.com/paper/2510.12047/) (2025)
- [David vs. Goliath: Can Small Models Win Big with Agentic AI in Hardware Design?](https://mlsanity.com/paper/2512.05073/) (2025)
- [MHRC-Bench: A Multilingual Hardware Repository-Level Code Completion benchmark](https://mlsanity.com/paper/2601.03708/) (2026)
- [FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification](https://mlsanity.com/paper/2604.03245/) (2026)
- [AutoAssert 1: A LoRA Fine-Tuned LLM Model for Efficient Automated Assertion Generation](https://mlsanity.com/paper/2508.07371/) (2025)
- [DUET: Agentic Design Understanding via Experimentation and Testing](https://mlsanity.com/paper/2512.06247/) (2025)
- [HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification](https://mlsanity.com/paper/2606.13706/) (2026)
- [Trust, but Validate the Instrument: Auditing AI-Generated RTL Verification Plans on Authored Security-Regression Proxies](https://mlsanity.com/paper/2609.19844/) (2026)
- [EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations](https://mlsanity.com/paper/2609.26751/) (2026)

## Abstract (arXiv)

Assertions have been the de facto collateral for simulation-based and formal verification of hardware designs for over a decade. The quality of hardware verification, ie, detection and diagnosis of corner-case design bugs, is critically dependent on the quality of the assertions. There has been a considerable amount of research leveraging a blend of data-driven statistical analysis and static analysis to generate high-quality assertions from hardware design source code and design execution trace data. Despite such concerted effort, all prior research struggles to scale to industrial-scale large designs, generates too many low-quality assertions, often fails to capture subtle and non-trivial design functionality, and does not produce any easy-to-comprehend explanations of the generated assertions to understand assertions' suitability to different downstream validation tasks. Recently, with the advent of Large-Language Models (LLMs), there has been a widespread effort to leverage prompt engineering to generate assertions. However, there is little effort to quantitatively establish the effectiveness and suitability of various LLMs for assertion generation. In this paper, we present AssertionBench, a novel benchmark to evaluate LLMs' effectiveness for assertion generation quantitatively. AssertioBench contains 100 curated Verilog hardware designs from OpenCores and formally verified assertions for each design generated from GoldMine and HARM. We use AssertionBench to compare state-of-the-art LLMs to assess their effectiveness in inferring functionally correct assertions for hardware designs. Our experiments demonstrate how LLMs perform relative to each other, the benefits of using more in-context exemplars in generating a higher fraction of functionally correct assertions, and the significant room for improvement for LLM-based assertion generators.