STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912974130642944 |
|---|---|
| author | Rajabi, Saeid Yang, Chengmo Patnaik, Satwik |
| author_facet | Rajabi, Saeid Yang, Chengmo Patnaik, Satwik |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_19903 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification Rajabi, Saeid Yang, Chengmo Patnaik, Satwik Hardware Architecture Artificial Intelligence 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. |
| title | STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification |
| topic | Hardware Architecture Artificial Intelligence |
| url | https://arxiv.org/abs/2601.19903 |