Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

AssertMiner: Module-Level Spec Generation and Assertion Mining using Static Analysis Guided LLMs

Hongqin Lyu, Yonghao Wang, Jiaxin Zhou, Zhiteng Chao, Tiancheng Wang, Huawei Li

TL;DR

AssertMiner tackles the shortage of module-level verification by coupling AST-derived structural analysis with LLM-based inference to generate per-module specifications and mine deep, module-local assertions. The four-stage framework first builds module-level structures (MCG, I/O, dataflow, signal chains), then derives module-specific specs and verification features, and finally mines unified deep assertions. Empirical results show stable module-spec generation, substantial deep-assertion coverage, and significant error-detection improvements when integrated with existing SOTA methods, validated on open RTL benchmarks with formal verification tooling. This approach enhances ABV by enabling finer-grained observation and faster debugging, with demonstrated potential to scale to more complex designs.

Abstract

Assertion-based verification (ABV) is a key approach to checking whether a logic design complies with its architectural specifications. Existing assertion generation methods based on design specifications typically produce only top-level assertions, overlooking verification needs on the implementation details in the modules at the micro-architectural level, where design errors occur more frequently. To address this limitation, we present AssertMiner, a module-level assertion generation framework that leverages static information generated from abstract syntax tree (AST) to assist LLMs in mining assertions. Specifically, it performs AST-based structural extraction to derive the module call graph, I/O table, and dataflow graph, guiding the LLM to generate module-level specifications and mine module-level assertions. Our evaluation demonstrates that AssertMiner outperforms existing methods such as AssertLLM and Spec2Assertion in generating high-quality assertions for modules. When integrated with these methods, AssertMiner can enhance the structural coverage and significantly improve the error detection capability, enabling a more comprehensive and efficient verification process.

AssertMiner: Module-Level Spec Generation and Assertion Mining using Static Analysis Guided LLMs

TL;DR

AssertMiner tackles the shortage of module-level verification by coupling AST-derived structural analysis with LLM-based inference to generate per-module specifications and mine deep, module-local assertions. The four-stage framework first builds module-level structures (MCG, I/O, dataflow, signal chains), then derives module-specific specs and verification features, and finally mines unified deep assertions. Empirical results show stable module-spec generation, substantial deep-assertion coverage, and significant error-detection improvements when integrated with existing SOTA methods, validated on open RTL benchmarks with formal verification tooling. This approach enhances ABV by enabling finer-grained observation and faster debugging, with demonstrated potential to scale to more complex designs.

Abstract

Assertion-based verification (ABV) is a key approach to checking whether a logic design complies with its architectural specifications. Existing assertion generation methods based on design specifications typically produce only top-level assertions, overlooking verification needs on the implementation details in the modules at the micro-architectural level, where design errors occur more frequently. To address this limitation, we present AssertMiner, a module-level assertion generation framework that leverages static information generated from abstract syntax tree (AST) to assist LLMs in mining assertions. Specifically, it performs AST-based structural extraction to derive the module call graph, I/O table, and dataflow graph, guiding the LLM to generate module-level specifications and mine module-level assertions. Our evaluation demonstrates that AssertMiner outperforms existing methods such as AssertLLM and Spec2Assertion in generating high-quality assertions for modules. When integrated with these methods, AssertMiner can enhance the structural coverage and significantly improve the error detection capability, enabling a more comprehensive and efficient verification process.

Paper Structure

This paper contains 19 sections, 7 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Related work
  3. Assertion Generation Based on NLP
  4. Assertion Generation Based on LLMs
  5. The Framework of AssertMiner
  6. Workflow Overview
  7. Step 1: AST-based structural analysis and signal chain generation
  8. Step 2: Module-Level Specification Extraction
  9. Step 3: Verification Feature Extraction for Modules
  10. Step 4: Deep Assertion Mining
  11. Experiments
  12. Experimental Setup
  13. Evaluation Metrics and Benchmarks
  14. Experimental Results
  15. Module-level Spec Generation Stability
  16. ...and 4 more sections

Figures (7)

  • Figure 1: A case of rapid assertion triggering and efficient debugging via assertion in the padder module of SHA3 b28.
  • Figure 2: The flowcharts of the AssertMiner framework for mining deep assertion, and the mined assertions are further evaluated against the golden RTL implementation using model checking tools.
  • Figure 4: Concise prompt and response of module-level specification extraction.
  • Figure 5: Example of decomposing moduel's spec into verification features
  • Figure 6:
  • ...and 2 more figures