AssertMiner: Module-Level Spec Generation and Assertion Mining using Static Analysis Guided LLMs
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908650285563904 |
|---|---|
| author | Lyu, Hongqin Wang, Yonghao Zhou, Jiaxin Chao, Zhiteng Wang, Tiancheng Li, Huawei |
| author_facet | Lyu, Hongqin Wang, Yonghao Zhou, Jiaxin Chao, Zhiteng Wang, Tiancheng Li, Huawei |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_10007 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | AssertMiner: Module-Level Spec Generation and Assertion Mining using Static Analysis Guided LLMs Lyu, Hongqin Wang, Yonghao Zhou, Jiaxin Chao, Zhiteng Wang, Tiancheng Li, Huawei Hardware Architecture 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. |
| title | AssertMiner: Module-Level Spec Generation and Assertion Mining using Static Analysis Guided LLMs |
| topic | Hardware Architecture |
| url | https://arxiv.org/abs/2511.10007 |