FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols

• URL: http://arxiv.org/abs/2504.17226v1
• Date: Thu, 24 Apr 2025 03:34:37 GMT
• Title: FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols
• Abstract summary: Formal specifications of on-chip communication protocols are crucial for system-on-chip (SoC) design and verification.<n>We propose FLAG, a two-stage framework to help construct formal protocol specifications from informal documents.
• Score: 2.242458166492809
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal specifications of on-chip communication protocols are crucial for system-on-chip (SoC) design and verification. However, manually constructing these formal specifications from informal documents remains a tedious and error-prone task. Although recent efforts have used Large Language Models (LLMs) to generate SystemVerilog Assertion (SVA) properties from design documents for Register-Transfer Level (RTL) design verification, in our experience these approaches have not shown promise in generating SVA properties for communication protocols. Since protocol specification documents are unstructured and ambiguous in nature, LLMs often fail to extract the necessary information and end up generating irrelevant or even incorrect properties. We propose FLAG, a two-stage framework to help construct formal protocol specifications from informal documents. In the first stage, a predefined template set is used to generate candidate SVA properties. To avoid missing necessary properties, we develop a grammar-based approach to generate comprehensive template sets that capture critical signal behaviors for various communication protocols. In the second stage, we utilize unambiguous timing diagrams in conjunction with textual descriptions from the specification documents to filter out incorrect properties. A formal approach is first implemented to check the candidate properties and filter out those inconsistent with the timing diagrams. An LLM is then consulted to further remove incorrect properties with respect to the textual description, obtaining the final property set. Experiments on various open-source communication protocols demonstrate the effectiveness of FLAG in generating SVA properties from informal documents.

Related papers

• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation [0.0]
  SystemVerilog Assertions (SVA) are essential for formal verification of digital hardware.<n>Recent studies have explored using large language models (LLMs) to automate SVA generation.<n>This paper presents ProofLoop, a tool-augmented ReAct agent that generates SVA from natural-language specifications.
  arXiv  Detail & Related papers  (2026-04-25T01:46:33Z)
• Understanding Contextual Recall in Transformers: How Finetuning Enables In-Context Reasoning over Pretraining Knowledge [50.009682083079205]
  We investigate whether contextual recall emerges from pretraining alone.<n>We show that finetuning on tasks requiring implicit inference, distinct from the ICL evaluation, triggers the emergence of contextual recall.<n>For mechanistic insight, we derive a construction for an attention-only transformer that replicates the transition from factual to contextual recall.
  arXiv  Detail & Related papers  (2026-03-21T22:46:55Z)
• Model-Document Protocol for AI Search [11.377241012645994]
  We introduce the Model-Document Protocol (MDP), a general framework that formalizes how raw text is bridged to large language models (LLMs)<n>Rather than treating retrieval as passage fetching, MDP defines multiple pathways that transform unstructured documents into task-specific, LLM-ready inputs.<n>As an instantiation, we present MDP-Agent, which realizes the protocol through an agentic process.
  arXiv  Detail & Related papers  (2025-10-29T04:29:17Z)
• Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? [1.9551668880584971]
  Large Language Models (LLMs) have shown promise in inferring formal postconditions from natural language hints.<n>We introduce NL2Contract, the task of employing LLMs to translate informal natural language into formal functional contracts.<n>We evaluate NL2Contract with different LLMs and compare it to the task of postcondition generation nl2postcond.
  arXiv  Detail & Related papers  (2025-10-14T16:37:39Z)
• Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams [54.528185120850274]
  We propose a novel step-by-step code generation framework named API2Dep.<n>First, we introduce an enhanced Unified Modeling Language (UML) API diagram tailored for service-oriented architectures.<n>Second, recognizing the critical role of data flow, we introduce a dedicated data dependency inference task.
  arXiv  Detail & Related papers  (2025-08-05T12:28:23Z)
• ModelForge: Using GenAI to Improve the Development of Security Protocols [1.9241821314180376]
  We introduce ModelForge, a novel tool that automates the translation of protocol specifications.<n>By leveraging advances in Natural Language Processing (NLP) and Generative AI (GenAI), ModelForge processes protocol specifications and generates a CPSA protocol definition.
  arXiv  Detail & Related papers  (2025-06-08T06:27:09Z)
• Validating Network Protocol Parsers with Traceable RFC Document Interpretation [11.081773172066766]
  oracle and traceability problems determine when a protocol implementation can be considered buggy. This work considers both and provides an effective solution using recent advances in large language models (LLMs) We have extensively evaluated our approach using nine network protocols and their implementations written in C, Python, and Go.
  arXiv  Detail & Related papers  (2025-04-25T03:39:19Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  We introduce a type-constrained decoding approach that leverages type systems to guide code generation.<n>For this purpose, we develop novel prefix automata and a search over inhabitable types, forming a sound approach to enforce well-typedness on LLM-generated code.<n>Our approach reduces compilation errors by more than half and significantly increases functional correctness in code synthesis, translation, and repair tasks.
  arXiv  Detail & Related papers  (2025-04-12T15:03:00Z)
• AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL [6.062811197376495]
  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.
  arXiv  Detail & Related papers  (2025-03-24T21:53:37Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [91.981439746404]
  We introduce QASemConsistency, a new formalism for localizing factual inconsistencies in attributable text generation. We first demonstrate the effectiveness of the QASemConsistency methodology for human annotation. We then implement several methods for automatically detecting localized factual inconsistencies.
  arXiv  Detail & Related papers  (2024-10-09T22:53:48Z)
• Object-Attribute Binding in Text-to-Image Generation: Evaluation and Control [58.37323932401379]
  Current diffusion models create images given a text prompt as input but struggle to correctly bind attributes mentioned in the text to the right objects in the image. We propose focused cross-attention (FCA) that controls the visual attention maps by syntactic constraints found in the input sentence. We show substantial improvements in T2I generation and especially its attribute-object binding on several datasets.
  arXiv  Detail & Related papers  (2024-04-21T20:26:46Z)
• Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach [3.9155346446573502]
  This paper introduces Auto-modeling of Formal Verification with Real-world Prompting for 5G and NextG protocols (AVRE) AVRE is a novel system designed for the formal verification of Next Generation (NextG) communication protocols.
  arXiv  Detail & Related papers  (2023-12-28T20:41:24Z)
• Validation of Rigorous Requirements Specifications and Document Automation with the ITLingo RSL Language [0.0]
  ITLingo initiative has introduced a requirements specification language named RSL to enhance the rigor and consistency of technical documentation. This paper reviews existing research and tools in the fields of requirements validation and document automation. We propose to extend RSL with validation of specifications based on customized checks, and on linguistic rules dynamically defined in the RSL itself.
  arXiv  Detail & Related papers  (2023-12-17T21:39:26Z)
• FLIP: Fine-grained Alignment between ID-based Models and Pretrained Language Models for CTR Prediction [49.510163437116645]
  Click-through rate (CTR) prediction plays as a core function module in personalized online services. Traditional ID-based models for CTR prediction take as inputs the one-hot encoded ID features of tabular modality. Pretrained Language Models(PLMs) has given rise to another paradigm, which takes as inputs the sentences of textual modality. We propose to conduct Fine-grained feature-level ALignment between ID-based Models and Pretrained Language Models(FLIP) for CTR prediction.
  arXiv  Detail & Related papers  (2023-10-30T11:25:03Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  Recent Language Models (LMs) have shown impressive capabilities in generating texts with the knowledge internalized in parameters. We propose to verify the output and the knowledge of the knowledge-augmented LMs with a separate verifier. Our results show that the proposed verifier effectively identifies retrieval and generation errors, allowing LMs to provide more factually correct outputs.
  arXiv  Detail & Related papers  (2023-10-19T15:40:00Z)
• Towards Formal Verification of a TPM Software Stack [0.5074812070492739]
  This paper describes a case study on formal verification of tpm2-tss using the Frama-C verification platform. Heavily based on linked lists and complex data structures, the library code appears to be highly challenging for the verification tool.
  arXiv  Detail & Related papers  (2023-07-31T16:35:16Z)
• MetricPrompt: Prompting Model as a Relevance Metric for Few-shot Text Classification [65.51149771074944]
  MetricPrompt eases verbalizer design difficulty by reformulating few-shot text classification task into text pair relevance estimation task. We conduct experiments on three widely used text classification datasets across four few-shot settings. Results show that MetricPrompt outperforms manual verbalizer and other automatic verbalizer design methods across all few-shot settings.
  arXiv  Detail & Related papers  (2023-06-15T06:51:35Z)
• Unified Pretraining Framework for Document Understanding [52.224359498792836]
  We present UDoc, a new unified pretraining framework for document understanding. UDoc is designed to support most document understanding tasks, extending the Transformer to take multimodal embeddings as input. An important feature of UDoc is that it learns a generic representation by making use of three self-supervised losses.
  arXiv  Detail & Related papers  (2022-04-22T21:47:04Z)
• SPECTER: Document-level Representation Learning using Citation-informed Transformers [51.048515757909215]
  SPECTER generates document-level embedding of scientific documents based on pretraining a Transformer language model. We introduce SciDocs, a new evaluation benchmark consisting of seven document-level tasks ranging from citation prediction to document classification and recommendation.
  arXiv  Detail & Related papers  (2020-04-15T16:05:51Z)

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.