# AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs

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

## Key facts

- Cited by 31 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Nov 2024.

## Built on by (most cited first, 30 of 31)

- [Adaptive Self-improvement LLM Agentic System for ML Library Development](https://mlsanity.com/paper/2502.02534/) (2025)
- [Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Dataset](https://mlsanity.com/paper/2503.08923/) (2025)
- [Revolution or Hype? Seeking the Limits of Large Models in Hardware Design](https://mlsanity.com/paper/2509.04905/) (2025)
- [NetDeTox: Adversarial and Efficient Evasion of Hardware-Security GNNs via RL-LLM Orchestration](https://mlsanity.com/paper/2512.00119/) (2025)
- [Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA](https://mlsanity.com/paper/2506.21569/) (2025)
- [ChatSVA: Bridging SVA Generation for Hardware Verification via Task-Specific LLMs](https://mlsanity.com/paper/2604.02811/) (2026)
- [HardSecBench: Benchmarking the Security Awareness of LLMs for Hardware Code Generation](https://mlsanity.com/paper/2601.13864/) (2026)
- [Large Language Models (LLMs) for Electronic Design Automation (EDA)](https://mlsanity.com/paper/2508.20030/) (2025)
- [Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation](https://mlsanity.com/paper/2601.19747/) (2026)
- [Semantic Consensus Decoding: Backdoor Defense for Verilog Code Generation](https://mlsanity.com/paper/2602.04195/) (2026)
- [Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification](https://mlsanity.com/paper/2605.06434/) (2026)
- [Reward-Weighted On-Policy Distillation with an Open Property-Equivalence Verifier for NL-to-SVA Generation](https://mlsanity.com/paper/2605.13501/) (2026)
- [Formalising Software Requirements using Large Language Models](https://mlsanity.com/paper/2506.10704/) (2025)
- [SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine](https://mlsanity.com/paper/2506.13983/) (2025)
- [EARL: Entropy-Aware RL Alignment of LLMs for Reliable RTL Code Generation](https://mlsanity.com/paper/2511.12033/) (2025)
- [QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis](https://mlsanity.com/paper/2603.14239/) (2026)
- [HAVEN: Hybrid Automated Verification ENgine for UVM Testbench Synthesis with LLMs](https://mlsanity.com/paper/2604.27643/) (2026)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)
- [STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification](https://mlsanity.com/paper/2601.19903/) (2025)
- [Evaluating LLM-Generated ACSL Annotations for Formal Verification](https://mlsanity.com/paper/2602.13851/) (2026)
- [SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation](https://mlsanity.com/paper/2605.25181/) (2026)
- [Faithful Autoformalization of Natural Language Assertions](https://mlsanity.com/paper/2607.13303/) (2026)
- [GoGoTB: Agentic RTL Verification with Specification-Grounded Coverage Closure](https://mlsanity.com/paper/2607.26181/) (2026)
- [NoTB: Oracle-Free Triage of LLM-Generated RTL via Cross-Model Formal Consensus](https://mlsanity.com/paper/2608.21962/) (2026)
- [Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations](https://mlsanity.com/paper/2609.05658/) (2026)
- [Working Document -- Formalising Software Requirements with Large Language Models](https://mlsanity.com/paper/2506.14627/) (2025)
- [Agentic AI-based Coverage Closure for Formal Verification](https://mlsanity.com/paper/2603.03147/) (2026)
- [Agentic Electronic Design Automation: A Handoff Perspective](https://mlsanity.com/paper/2606.19795/) (2026)
- [LLM for EDA in Front-End Design: Challenges and Opportunities](https://mlsanity.com/paper/2607.09616/) (2026)
- [Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement](https://mlsanity.com/paper/2608.18482/) (2026)

## Abstract (arXiv)

Assertion-based verification (ABV) is a critical method to ensure logic designs comply with their architectural specifications. ABV requires assertions, which are generally converted from specifications through human interpretation by verification engineers. Existing methods for generating assertions from specification documents are limited to sentences extracted by engineers, discouraging their practical applications. In this work, we present AssertLLM, an automatic assertion generation framework that processes complete specification documents. AssertLLM can generate assertions from both natural language and waveform diagrams in specification files. It first converts unstructured specification sentences and waveforms into structured descriptions using natural language templates. Then, a customized Large Language Model (LLM) generates the final assertions based on these descriptions. Our evaluation demonstrates that AssertLLM can generate more accurate and higher-quality assertions compared to GPT-4o and GPT-3.5.