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

• URL: http://arxiv.org/abs/2503.19174v1
• Date: Mon, 24 Mar 2025 21:53:37 GMT
• Title: AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL
• Authors: Yunsheng Bai, Ghaith Bany Hamad, Syed Suhaib, Haoxing Ren,
• Abstract summary: We propose a novel approach that constructs a Knowledge Graph (KG) from both specifications and RTL.<n>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.<n> Experiments on four designs demonstrate that our method significantly enhances SVA quality over prior methods.
• Score: 6.062811197376495
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• LightPROF: A Lightweight Reasoning Framework for Large Language Model on Knowledge Graph [57.382255728234064]
  Large Language Models (LLMs) have impressive capabilities in text understanding and zero-shot reasoning. Knowledge Graphs (KGs) provide rich and reliable contextual information for the reasoning process of LLMs. We propose a novel Lightweight and efficient Prompt learning-ReasOning Framework for KGQA (LightPROF)
  arXiv  Detail & Related papers  (2025-04-04T03:03:47Z)
• Post-Incorporating Code Structural Knowledge into LLMs via In-Context Learning for Code Translation [10.77747590700758]
  Large language models (LLMs) have achieved significant advancements in software mining. handling the syntactic structure of source code remains a challenge. This paper employs incontext learning (ICL) to integrate code structural knowledge into pre-trained LLMs.
  arXiv  Detail & Related papers  (2025-03-28T10:59:42Z)
• Aligning Vision to Language: Text-Free Multimodal Knowledge Graph Construction for Enhanced LLMs Reasoning [10.761218096540976]
  Multimodal reasoning in Large Language Models (LLMs) struggles with incomplete knowledge and hallucination artifacts.<n>We propose Vision-align-to-Language integrated Knowledge Graph (VaLiK), a novel approach for constructing Multimodal Knowledge Graphs.
  arXiv  Detail & Related papers  (2025-03-17T09:31:14Z)
• OmniParser V2: Structured-Points-of-Thought for Unified Visual Text Parsing and Its Generality to Multimodal Large Language Models [58.45517851437422]
  Visually-situated text parsing (VsTP) has recently seen notable advancements, driven by the growing demand for automated document understanding.<n>Existing solutions often rely on task-specific architectures and objectives for individual tasks.<n>In this paper, we introduce Omni V2, a universal model that unifies VsTP typical tasks, including text spotting, key information extraction, table recognition, and layout analysis.
  arXiv  Detail & Related papers  (2025-02-22T09:32:01Z)
• Oreo: A Plug-in Context Reconstructor to Enhance Retrieval-Augmented Generation [28.568010424711563]
  Large Language Models (LLMs) remain vulnerable to hallucinations due to their limited parametric knowledge and lack of domain-specific expertise.<n>Retrieval-Augmented Generation (RAG) addresses this challenge by incorporating external document retrieval to augment the knowledge base of LLMs.<n>We introduce a compact, efficient, and pluggable module designed to refine external knowledge sources before feeding them to the generator.
  arXiv  Detail & Related papers  (2025-02-18T16:38:39Z)
• Self-supervised Quantized Representation for Seamlessly Integrating Knowledge Graphs with Large Language Models [17.88134311726175]
  We propose a framework to learn and apply quantized codes for each entity, aiming for the seamless integration of Knowledge Graphs with Large Language Models.<n>Experiment results demonstrate that SSQR outperforms existing unsupervised quantized methods, producing more distinguishable codes.<n>The fine-tuned LLaMA2 and LLaMA3.1 also have superior performance on KG link prediction and triple classification tasks.
  arXiv  Detail & Related papers  (2025-01-30T03:40:20Z)
• ForgeryGPT: Multimodal Large Language Model For Explainable Image Forgery Detection and Localization [49.12958154544838]
  ForgeryGPT is a novel framework that advances the Image Forgery Detection and localization task.<n>It captures high-order correlations of forged images from diverse linguistic feature spaces.<n>It enables explainable generation and interactive dialogue through a newly customized Large Language Model (LLM) architecture.
  arXiv  Detail & Related papers  (2024-10-14T07:56:51Z)
• Contextualization Distillation from Large Language Model for Knowledge Graph Completion [51.126166442122546]
  We introduce the Contextualization Distillation strategy, a plug-in-and-play approach compatible with both discriminative and generative KGC frameworks. Our method begins by instructing large language models to transform compact, structural triplets into context-rich segments. Comprehensive evaluations across diverse datasets and KGC techniques highlight the efficacy and adaptability of our approach.
  arXiv  Detail & Related papers  (2024-01-28T08:56:49Z)
• From Dialogue to Diagram: Task and Relationship Extraction from Natural Language for Accelerated Business Process Prototyping [0.0]
  This paper introduces a contemporary solution, where central to our approach, is the use of dependency parsing and Named Entity Recognition (NER) We utilize Subject-Verb-Object (SVO) constructs for identifying action relationships and integrate semantic analysis tools, including WordNet, for enriched contextual understanding. The system adeptly handles data transformation and visualization, converting verbose extracted information into BPMN (Business Process Model and Notation) diagrams.
  arXiv  Detail & Related papers  (2023-12-16T12:35:28Z)
• Unifying Structure and Language Semantic for Efficient Contrastive Knowledge Graph Completion with Structured Entity Anchors [0.3913403111891026]
  The goal of knowledge graph completion (KGC) is to predict missing links in a KG using trained facts that are already known. We propose a novel method to effectively unify structure information and language semantics without losing the power of inductive reasoning.
  arXiv  Detail & Related papers  (2023-11-07T11:17:55Z)
• Universal Information Extraction as Unified Semantic Matching [54.19974454019611]
  We decouple information extraction into two abilities, structuring and conceptualizing, which are shared by different tasks and schemas. Based on this paradigm, we propose to universally model various IE tasks with Unified Semantic Matching framework. In this way, USM can jointly encode schema and input text, uniformly extract substructures in parallel, and controllably decode target structures on demand.
  arXiv  Detail & Related papers  (2023-01-09T11:51:31Z)
• Schema-aware Reference as Prompt Improves Data-Efficient Knowledge Graph Construction [57.854498238624366]
  We propose a retrieval-augmented approach, which retrieves schema-aware Reference As Prompt (RAP) for data-efficient knowledge graph construction. RAP can dynamically leverage schema and knowledge inherited from human-annotated and weak-supervised data as a prompt for each sample.
  arXiv  Detail & Related papers  (2022-10-19T16:40:28Z)
• Knowledge Graph Augmented Network Towards Multiview Representation Learning for Aspect-based Sentiment Analysis [96.53859361560505]
  We propose a knowledge graph augmented network (KGAN) to incorporate external knowledge with explicitly syntactic and contextual information. KGAN captures the sentiment feature representations from multiple perspectives, i.e., context-, syntax- and knowledge-based. Experiments on three popular ABSA benchmarks demonstrate the effectiveness and robustness of our KGAN.
  arXiv  Detail & Related papers  (2022-01-13T08:25:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.