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

TL;DR

This paper tackles the challenge of deriving formal protocol specifications from informal on-chip communication documents. It introduces FLAG, a two-stage framework that first uses grammar- and template-based generation to produce candidate SystemVerilog Assertions (SVAs), and then applies a formal SAT-based check against unambiguous timing diagrams followed by an LLM-assisted filtering against textual descriptions to prune incorrect properties. The approach yields a compact, correct, and extensible property set across multiple open-source protocols, outperforming purely ML-based baselines and reducing reliance on manual specification. The work demonstrates practical impact by enabling scalable, reproducible formal specifications for complex SoC protocols, with potential to improve verification reliability and maintainability.

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.

Figures (5)

• Figure 1: Example of an ambiguous statement. An ML model may intuitively translate "remain stable" into the $stable operator in SVA. However, the "remain stable" in this context actually means "assign the same value in the next clock cycle," i.e., the $stable operator should be delayed by one cycle.
• Figure 2: The Flag framework.
• Figure 3: Example of timing diagrams extracted from the AMBA AXI Protocol Specification spec:axi.
• Figure 4: Example of a template and some of its candidate properties generated by the property generation algorithm.
• Figure 5: Example of a simple grammar, where the top-level rule is $\langle$implic$\rangle$, and the terminals are (1) SVA operators and (2) signal (<signal>, <word>) and value (<level>) types.