用知识图谱融合规格与硬件代码，提升验证断言生成质量。
AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL
- 构建规格与RTL的联合知识图谱，捕获设计内部信号关系。
- 在4个设计上验证，断言生成质量显著优于现有方法。
- 适合形式化验证工程师及芯片设计自动化研究者。
从自然语言规格生成SystemVerilog断言（SVAs）在形式化验证中仍面临挑战，主要因规格存在歧义和不完整。现有基于大模型的方法（如AssertLLM）仅依赖规格文档，难以捕捉RTL代码中的关键信号交互与设计细节，导致断言不完整或错误。本文提出一种新方法：从规格和RTL共同构建硬件专用知识图谱（KG），采用领域特定的实体与关系类型；先基于规格构建初始KG，再系统融合从RTL提取的信息，形成统一、全面的表示。该结构化表示支持多粒度上下文合成，可更深入理解设计。在4个设计上的实验表明，本方法显著提升了SVA质量。该表示不仅增强形式化验证，也为代码生成与设计理解等任务提供新路径。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。