2601.19903

Total: 1

#1 STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification [PDF] [Copy] [Kimi1] [REL]

Authors: Saeid Rajabi, Chengmo Yang, Satwik Patnaik

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.

Subjects: Hardware Architecture , Artificial Intelligence

Publish: 2025-11-28 05:31:07 UTC