# Are LLMs Ready for Practical Adoption for Assertion Generation?

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 42 references that are in the map.
- First posted on arXiv 28 Feb 2025.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [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)
- [CodeBERT: A Pre-Trained Model for Programming and Natural Languages](https://mlsanity.com/paper/2002.08155/) (2020)
- [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)
- [AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2402.00386/) (2024)
- [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)
- [AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation](https://mlsanity.com/paper/2406.18627/) (2024)
- [Isadora: Automated Information Flow Property Generation for Hardware Designs](https://mlsanity.com/paper/2106.07449/) (2021)

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

- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)
- [Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification](https://mlsanity.com/paper/2605.06434/) (2026)
- [UCAgent: An End-to-End Agent for Block-Level Functional Verification](https://mlsanity.com/paper/2603.25768/) (2026)
- [STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification](https://mlsanity.com/paper/2601.19903/) (2025)
- [SeqFeed: Improving Agentic RTL Code Generation with Sequential Behavior Feedback](https://mlsanity.com/paper/2608.16934/) (2026)
- [A Survey on LLM-Integrated Hardware Design Verification](https://mlsanity.com/paper/2610.10580/) (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, i.e., detection and diagnosis of corner-case design bugs, is critically dependent on the quality of the assertions. With the onset of generative AI such as Transformers and Large-Language Models (LLMs), there has been a renewed interest in developing novel, effective, and scalable techniques of generating functional and security assertions from design source code. While there have been recent works that use commercial-of-the-shelf (COTS) LLMs for assertion generation, there is no comprehensive study in quantifying the effectiveness of LLMs in generating syntactically and semantically correct assertions. In this paper, we first discuss AssertionBench from our prior work, a comprehensive set of designs and assertions to quantify the goodness of a broad spectrum of COTS LLMs for the task of assertion generations from hardware design source code. Our key insight was that COTS LLMs are not yet ready for prime-time adoption for assertion generation as they generate a considerable fraction of syntactically and semantically incorrect assertions. Motivated by the insight, we propose AssertionLLM, a first of its kind LLM model, specifically fine-tuned for assertion generation. Our initial experimental results show that AssertionLLM considerably improves the semantic and syntactic correctness of the generated assertions over COTS LLMs.