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

TL;DR

AssertionForge tackles the challenge of generating correct SVAs from ambiguous natural language specifications by building a unified Knowledge Graph from both specifications and RTL. It introduces a hardware-specific KG construction via GraphRAG, RTL refinement with a PyVerilog-based parser, and a multi-resolution context synthesis pipeline, including GRW-AS guided walks and an LLM-based pruner. The approach yields substantial improvements in SVA quality and coverage across five designs, outperforming specification-only LLM methods and RTL-only baselines. This structured representation enhances formal verification and opens avenues for code generation and deeper design understanding.

Abstract

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.

Figures (14)

• Figure 1: Overview of AssertionForge. Our method is structured into a three-stage process: First, we construct a domain-specific Knowledge Graph (KG) that captures the essential entities and relationships in the design. Together with the raw specifications and RTL, we build a mental model for the design under verification. Second, we generate three types of candidate contexts for each signal. Lastly, we use these contexts to dynamically construct prompts for a Large Language Model (LLM) to generate accurate SVAs.
• Figure 2: Visualization of the KGs from openMSP430 using ICWSM09154. Node colors represent different types of entities, such as modules and signals. Node colors indicate the type attribute of each entity. Left: KG generated via the original entity extraction prompt of GraphRAG. Middle: KG generated via our domain-customized prompt. Right: Two zoomed-in views of the KG, highlighting key entities with their labels.
• Figure 3: Examples of SVAs generated by AssertionForge.
• Figure 4: Example prompt for entity extraction (abbreviated). For the full prompt, see: https://github.com/microsoft/graphrag/blob/main/graphrag/index/graph/extractors/graph/prompts.py
• Figure 5: Prompt for generating a high-level design specification summary. The prompt emphasizes conciseness while focusing on functionality, key components, and architecture.