Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification

Saeid Rajabi, Chengmo Yang, Satwik Patnaik

TL;DR

STELLAR tackles the challenge of automating SystemVerilog Assertion generation for formal verification by leveraging structure-aware retrieval from a large RTL-SVA knowledge base. It introduces AST-based structural fingerprints to find structurally similar RTL/SVA pairs and guides LLMs through structure-guided prompting to produce high-coverage, stylistically consistent SVAs. The framework operates with an offline knowledge base construction phase and an online SVA generation phase, enabling scalability without model retraining. Experiments on the VERT dataset across multiple LLMs show improved syntax correctness, semantic alignment, and formal coverage, validating structure-aware retrieval as a practical approach for industrial formal verification.

Abstract

Formal Verification (FV) relies on high-quality SystemVerilog Assertions (SVAs), but the manual writing process is slow and error-prone. Existing LLM-based approaches either generate assertions from scratch or ignore structural patterns in hardware designs and expert-crafted assertions. This paper presents STELLAR, the first framework that guides LLM-based SVA generation with structural similarity. STELLAR represents RTL blocks as AST structural fingerprints, retrieves structurally relevant (RTL, SVA) pairs from a knowledge base, and integrates them into structure-guided prompts. Experiments show that STELLAR achieves superior syntax correctness, stylistic alignment, and functional correctness, highlighting structure-aware retrieval as a promising direction for industrial FV.

STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification

TL;DR

STELLAR tackles the challenge of automating SystemVerilog Assertion generation for formal verification by leveraging structure-aware retrieval from a large RTL-SVA knowledge base. It introduces AST-based structural fingerprints to find structurally similar RTL/SVA pairs and guides LLMs through structure-guided prompting to produce high-coverage, stylistically consistent SVAs. The framework operates with an offline knowledge base construction phase and an online SVA generation phase, enabling scalability without model retraining. Experiments on the VERT dataset across multiple LLMs show improved syntax correctness, semantic alignment, and formal coverage, validating structure-aware retrieval as a practical approach for industrial formal verification.

Abstract

Formal Verification (FV) relies on high-quality SystemVerilog Assertions (SVAs), but the manual writing process is slow and error-prone. Existing LLM-based approaches either generate assertions from scratch or ignore structural patterns in hardware designs and expert-crafted assertions. This paper presents STELLAR, the first framework that guides LLM-based SVA generation with structural similarity. STELLAR represents RTL blocks as AST structural fingerprints, retrieves structurally relevant (RTL, SVA) pairs from a knowledge base, and integrates them into structure-guided prompts. Experiments show that STELLAR achieves superior syntax correctness, stylistic alignment, and functional correctness, highlighting structure-aware retrieval as a promising direction for industrial FV.
Paper Structure (23 sections, 6 figures, 5 tables)

This paper contains 23 sections, 6 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Background and Related Works
  3. Automated Assertion Generation
  4. Retrieval-Augmented Generation (RAG)
  5. LLM Interaction Paradigms
  6. Hardware Similarity and Structural Representations
  7. Dataset Generation for Assertion Learning
  8. Methodology: STELLAR Framework
  9. Structural Fingerprinting
  10. Structural Embeddings and Retrieval
  11. Structure-Guided Prompting
  12. SVA Generation Using LLMs
  13. Putting It All Together
  14. Experimental Setup
  15. Implementation Details
  16. ...and 8 more sections

Figures (6)

  • Figure 1: Structural vs. semantic retrieval: S1 (different names, same control-flow) structure-aware correctly matches but semantic may miss; S2 (different control-flow, same name) semantic has a false hit while structure-aware separates.
  • Figure 2: Collision comparison for HW2VEC yu2021hw2vec embeddings and STELLAR structural fingerprinting (lesser is better).
  • Figure 3: Query runtime for raw string match (RAW) vs. embedding retrieval using brute-force and FAISS indexing.
  • Figure 4: Structure-guided prompting: left = without, right = with.
  • Figure 5: Execution-path coverage (higher is better)
  • ...and 1 more figures