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 is a static analysis-guided framework that enhances assertion generation at the module level using LLMs, improving verification coverage and error detection in hardware design.
Contribution
It introduces a novel static analysis-guided approach for module-level assertion mining using LLMs, addressing limitations of top-level assertion generation methods.
Findings
Outperforms existing assertion generation methods like AssertLLM and Spec2Assertion.
Enhances structural coverage and error detection capabilities.
Enables more comprehensive and efficient verification processes.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Logic, programming, and type systems
