# AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL

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

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- Builds on 35 of its 83 references that are in the map.
- First posted on arXiv 24 Mar 2025.

## Builds on (most cited first, 30 of 35)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks](https://mlsanity.com/paper/1908.10084/) (2019)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [node2vec: Scalable Feature Learning for Networks](https://mlsanity.com/paper/1607.00653/) (2016)
- [From Local to Global: A Graph RAG Approach to Query-Focused Summarization](https://mlsanity.com/paper/2404.16130/) (2024)
- [Improving language models by retrieving from trillions of tokens](https://mlsanity.com/paper/2112.04426/) (2021)
- [Unifying Large Language Models and Knowledge Graphs: A Roadmap](https://mlsanity.com/paper/2306.08302/) (2023)
- [A Survey on Knowledge Graphs: Representation, Acquisition and Applications](https://mlsanity.com/paper/2002.00388/) (2020)
- [NV-Embed: Improved Techniques for Training LLMs as Generalist Embedding Models](https://mlsanity.com/paper/2405.17428/) (2024)
- [COMET: Commonsense Transformers for Automatic Knowledge Graph Construction](https://mlsanity.com/paper/1906.05317/) (2019)
- [Graph Retrieval-Augmented Generation: A Survey](https://mlsanity.com/paper/2408.08921/) (2024)
- [Knowledge Graph Prompting for Multi-Document Question Answering](https://mlsanity.com/paper/2308.11730/) (2023)
- [Deeper Text Understanding for IR with Contextual Neural Language Modeling](https://mlsanity.com/paper/1905.09217/) (2019)
- [A Survey of Knowledge Graph Reasoning on Graph Types: Static, Dynamic, and Multimodal](https://mlsanity.com/paper/2212.05767/) (2022)
- [LLMs for Knowledge Graph Construction and Reasoning: Recent Capabilities and Future Opportunities](https://mlsanity.com/paper/2305.13168/) (2023)
- [HybridRAG: Integrating Knowledge Graphs and Vector Retrieval Augmented Generation for Efficient Information Extraction](https://mlsanity.com/paper/2408.04948/) (2024)
- [Domain-specific Knowledge Graphs: A survey](https://mlsanity.com/paper/2011.00235/) (2020)
- [A Comprehensive Survey on Automatic Knowledge Graph Construction](https://mlsanity.com/paper/2302.05019/) (2023)
- [Generative Knowledge Graph Construction: A Review](https://mlsanity.com/paper/2210.12714/) (2022)
- [Enhancing Knowledge Graph Construction Using Large Language Models](https://mlsanity.com/paper/2305.04676/) (2023)
- [(Security) Assertions by Large Language Models](https://mlsanity.com/paper/2306.14027/) (2023)
- [AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2402.00386/) (2024)
- [CodeKGC: Code Language Model for Generative Knowledge Graph Construction](https://mlsanity.com/paper/2304.09048/) (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)
- [Combining Knowledge Graphs and Large Language Models](https://mlsanity.com/paper/2407.06564/) (2024)
- [AutoSVA: Democratizing Formal Verification of RTL Module Interactions](https://mlsanity.com/paper/2104.04003/) (2021)
- [Self-HWDebug: Automation of LLM Self-Instructing for Hardware Security Verification](https://mlsanity.com/paper/2405.12347/) (2024)
- [FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware](https://mlsanity.com/paper/2410.23299/) (2024)

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

- [SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Models](https://mlsanity.com/paper/2506.20415/) (2025)
- [ChatSVA: Bridging SVA Generation for Hardware Verification via Task-Specific LLMs](https://mlsanity.com/paper/2604.02811/) (2026)
- [TB or Not TB: Coverage-Driven Direct Preference Optimization for Verilog Stimulus Generation](https://mlsanity.com/paper/2511.15767/) (2025)
- [Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification](https://mlsanity.com/paper/2605.06434/) (2026)
- [AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications](https://mlsanity.com/paper/2605.27472/) (2026)
- [QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis](https://mlsanity.com/paper/2603.14239/) (2026)
- [STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification](https://mlsanity.com/paper/2601.19903/) (2025)
- [VeriGraphi: A Multi-Agent Framework of Hierarchical RTL Generation for Large Hardware Designs](https://mlsanity.com/paper/2604.14550/) (2026)
- [SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation](https://mlsanity.com/paper/2605.25181/) (2026)
- [RTL-BenchLS: A Large-Scale Benchmark for RTL Reasoning and Generation with Large Language Models](https://mlsanity.com/paper/2606.08976/) (2026)
- [Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations](https://mlsanity.com/paper/2609.05658/) (2026)
- [Autoformalizing Memory Specifications with Agents](https://mlsanity.com/paper/2605.00058/) (2026)
- [HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification](https://mlsanity.com/paper/2606.13706/) (2026)

## Abstract (arXiv)

Generating SystemVerilog Assertions (SVAs) from natural language specifications remains a major challenge in formal verification (FV) due to the inherent ambiguity and incompleteness of specifications. Existing LLM-based approaches, such as AssertLLM, focus on extracting information solely from specification documents, often failing to capture essential internal signal interactions and design details present in the RTL code, leading to incomplete or incorrect assertions. We propose a novel approach that constructs a Knowledge Graph (KG) from both specifications and RTL, using a hardware-specific schema with domain-specific entity and relation types. We create an initial KG from the specification and then systematically fuse it with information extracted from the RTL code, resulting in a unified, comprehensive KG. This combined representation enables a more thorough understanding of the design and allows for a multi-resolution context synthesis process which is designed to extract diverse verification contexts from the KG. Experiments on four designs demonstrate that our method significantly enhances SVA quality over prior methods. This structured representation not only improves FV but also paves the way for future research in tasks like code generation and design understanding.