DeepAssert: An LLM-Aided Verification Framework with Fine-Grained Assertion Generation for Modules with Extracted Module Specifications
Open accessAbstract
Assertion-Based Verification (ABV) is a crucial method for ensuring that logic designs conform to their architectural specifications. However, existing assertion generation methods primarily rely on information either from the design specification, or register-transfer level (RTL) code. The former methods are typically limited to generating assertions for the top-level design. As the top-level design is composed of different modules without module-level specifications, they are unable to generate deep assertions that target the internal functionality of modules. The latter methods often rely on a golden RTL model, which is difficult to obtain. To address the above limitations, this paper presents a novel large language model (LLM)-aided verification framework named DeepAssert. DeepAssert is capable of analyzing the invocation relationships between modules and extracting independent specifications for each module with its I/O port information. These extracted specifications are subsequently used to guide LLMs to automatically generate fine-grained deep assertions for these modules. Our evaluation demonstrates that DeepAssert significantly outperforms existing methods such as AssertLLM and Spec2Assertion in generating high-quality deep assertions for modules. Furthermore, when integrated with these methods, DeepAssert can enhance the overall quality of the assertions generated. This allows for a more comprehensive and effective verification process.
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
The key bottleneck of certificate-based verification is certificate quality: current LLMs often fail to produce properties that are both verifiable and complete enough to exclude incorrect behaviors.
“Their key bottleneck is certificate quality: current LLMs often fail to produce properties that are both verifiable and complete enough to exclude incorrect behaviors [18], [70], [71].”
From Guiding Human Validation of LLM-Generated Code via Verifiable Literate Programming (2026) · cites this paper as [18]
The Introduction (pp. 1–2) says LLM-generated hardware assertions can miss critical implementation details or inherit RTL errors, and that top-level assertions can fail to verify internal module behavior. This supports a concern about assertion quality and coverage, but the paper does not frame it as a bottleneck in certificate-based verification or establish that LLMs often fail to produce properties that are both verifiable and complete enough to exclude incorrect behaviors. (LLM, conf=0.83)
Experimental — accuracy not yet measured
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Cites
No references could be resolved yet.
Research works printed but not linked: 17
- [3][3] Yael Abarbanel, Ilan Beer, Leonid Gluhovsky, Sharon Keidar, and Yaron Wolfsthal. Focs-automatic generation of simulation checkers from formal specifications. In Computer Aided Verification: 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000. Proceedings 12 , pages 538-542. Springer, 2000. -
- [4][4] Fnu Aditi and Michael S Hsiao. Hybrid rule-based and machine learning system for assertion generation from natural language specifications. In 2022 IEEE 31st Asian Test Symposium (ATS) , pages 126-131. IEEE, 2022. -
- [5][5] Amira A Alshazly, Ahmed M Elfatatry, and Mohamed S Abougabal. Detecting defects in software requirements specification. Alexandria Engineering Journal , 53(3):513-527, 2014. -
- [6][6] Yunsheng Bai, Ghaith Bany Hamad, Syed Suhaib, and Haoxing Ren. Assertionforge: Enhancing formal verification assertion generation with structured representation of specifications and rtl. arXiv preprint arXiv:2503.19174 , 2025. - · arXiv
- [7][7] Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In International Conference on Computer Aided Verification , pages 383396. Springer, 2023. -
- [8][8] Wenji Fang, Mengming Li, Min Li, Zhiyuan Yan, Shang Liu, Zhiyao Xie, and Hongce Zhang. Assertllm: Generating and evaluating hardware verification assertions from design specifications via multi-llms. arXiv preprint arXiv:2402.00386 , 2024. - · arXiv
- [10][10] Harry Foster. Assertion-based verification: Industry myths to realities (invited tutorial). In Computer Aided Verification: 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings 20 , pages 5-10. Springer, 2008. -
- [11][11] Eugene Goldberg. Generation of a complete set of properties. arXiv preprint arXiv:2004.05853 , 2020. - · arXiv
- [12][12] Rahul Kande, Hammond Pearce, Benjamin Tan, Brendan Dolan-Gavitt, Shailja Thakur, Ramesh Karri, and Jeyavijayan Rajendran. (security) assertions by large language models. IEEE Transactions on Information Forensics and Security , 2024. -
- [13][13] Mengming Li, Wenji Fang, Qijun Zhang, and Zhiyao Xie. Specllm: Exploring generation and review of vlsi design specification with large language model. arXiv preprint arXiv:2401.13266 , 2024. - · arXiv
- [14][14] Vaishnavi Pulavarthi, Deeksha Nandal, Soham Dan, and Debjit Pal. Are llms ready for practical adoption for assertion generation? In 2025 Design, Automation & Test in Europe Conference (DATE) , pages 1-7. IEEE, 2025. -
- [15][15] Hafiz Abdul Quddus, Md Sanowar Hossain, Ziya Cevahir, Alexander Jesser, and Md Nur Amin. Enhanced vlsi assertion generation: Conforming to high-level specifications and reducing llm hallucinations with rag. In DVCon Europe 2024; Design and Verification Conference and Exhibition Europe , pages 57-62. VDE, 2024. -
- [16][16] Erik Seligman, Tom Schubert, and MV Achutha Kiran Kumar. Formal verification: an essential toolkit for modern VLSI design . Elsevier, 2023. -
- [17][17] Chuyue Sun, Christopher Hahn, and Caroline Trippel. Towards improving verification productivity with circuit-aware translation of natural language to systemverilog assertions. In First International Workshop on Deep Learning-aided Verification , 2023. -
- [18][18] Hasini Witharana, Yangdi Lyu, Subodha Charles, and Prabhat Mishra. A survey on assertion-based hardware verification. ACM Computing Surveys (CSUR) , 54(11s):1-33, 2022. -
- [19][19] Fenghua Wu, Evan Pan, Rahul Kande, Michael Quinn, Aakash Tyagi, David Kebo, Jeyavijayan Rajendran, and Jiang Hu. Spec2assertion: Automatic pre-rtl assertion generation using large language models with progressive regularization. arXiv preprint arXiv:2505.07995 , 2025. - · arXiv
- [20][20] Quanjun Zhang, Weifeng Sun, Chunrong Fang, Bowen Yu, Hongyan Li, Meng Yan, Jianyi Zhou, and Zhenyu Chen. Exploring automated assertion generation via large language models. ACM Transactions on Software Engineering and Methodology , 34(3):1-25, 2025.
Cited by
Sorted by citations
Guiding Human Validation of LLM-Generated Code via Verifiable Literate Programming
Yuan, Z., Lu, W., Wu, H., Jin, D., & Wu, C. (2026) · arXiv · doi:10.48550/arxiv.2607.02333
- Authors
- Wang, Y., Zhou, J., Lyu, H., Chao, Z., Wang, T., & Li, H.
- Venue
- arXiv
- Publisher
- arXiv
- Published
- 2025
- ISSN
- 2331-8422 (ISSN-L)
- arXiv
- 2509.14668
- OpenAlex
- W4417081733
- Cited by
- 0
- References
- 0
- Type
- posted content
- Language
- en
- Open access
- green
- arxiv.org
- Locations
- arXiv (Cornell University) (submittedVersion)
- arXiv (Cornell University)
- Topics
- Physical Sciences › Computer Science › Hardware and Architecture › Embedded Systems Design Techniques
- Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Keywords
- assertion-based verification, large language models, hardware verification, digital circuit design
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
