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

TL;DR

STELLAR is a novel framework that enhances formal verification by guiding large language models to generate high-quality assertions using structural similarity of hardware designs, improving correctness and style.

Contribution

It introduces a structure-guided retrieval and generation approach for SystemVerilog Assertions, leveraging AST fingerprints to improve assertion quality in formal verification.

Findings

Achieves higher syntax correctness in generated assertions

Improves stylistic and functional alignment with expert assertions

Demonstrates the effectiveness of structure-aware retrieval in industrial FV

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.