AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL
This work addresses a major problem in formal verification for hardware design engineers, representing an incremental improvement over existing LLM-based approaches.
The paper tackles the challenge of generating SystemVerilog Assertions from natural language specifications by constructing a Knowledge Graph from both specifications and RTL code, which significantly enhances assertion quality over prior methods, as demonstrated in experiments on four designs.
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.