The DOI matches its Crossref record; 9 of the 11 references it cites were found in a registry or an index.
LLM-Guided Formal Verification Coupled with Mutation Testing
Abstract
The increasing complexity of modern hardware designs poses significant challenges for design verification, particularly defining and verifying properties and invariants manually. Recently, Large Language Models (LLMs) such has GPT-4 have been explored to generate these properties. However, assessing the quality of these LLM generated properties is still lacking. In this paper, we introduce a LLM-guided formal verification methodology combined with mutation testing for creating and assessing invariants for Design Under Verification (DUV). Utilizing OpenAI's GPT-4, we automate the generation of invariants and formal models from design specifications and Verilog behavioral models, respectively. We further enhance this approach with mutation testing to validate the quality of the invariants. We use a 27-channel interrupt controller (C432) from ISCAS-85 benchmarks as a complex case-study to showcase the methodology.
Overview
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
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?
In the citing paper
“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 [71]
Citations
Cites
An Analysis and Survey of the Development of Mutation Testing
Jia, Y., & Harman, M. (2010) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2010.62 · Cited by 1,853
Unveiling the ISCAS-85 benchmarks: a case study in reverse engineering
Hansen, M. C., Yalcin, H., & Hayes, J. P. (1999) · IEEE Design & Test of Computers · doi:10.1109/54.785838 · Cited by 541
Chip-Chat: Challenges and Opportunities in Conversational Hardware Design
Blocklove, J., Garg, S., Karri, R., & Pearce, H. A. (2023) · ACM/IEEE Workshop on Machine Learning for CAD (MLCAD) · doi:10.1109/mlcad58807.2023.10299874 · Cited by 286
(Security) Assertions by Large Language Models
Kande, R., Pearce, H. A., Tan, B., Dolan-Gavitt, B., Thakur, S., Karri, R., & Rajendran, J. (2024) · IEEE Transactions on Information Forensics and Security · doi:10.1109/tifs.2024.3372809 · Cited by 160
Drechsler, R. (2004) · Springer eBooks · doi:10.1007/b105236 · Cited by 156
Self-citationOn Hardware Security Bug Code Fixes by Prompting Large Language Models
Ahmad, B., Thakur, S., Tan, B., Karri, R., & Pearce, H. A. (2024) · IEEE Transactions on Information Forensics and Security · doi:10.1109/tifs.2024.3374558 · Cited by 149
LLM for SoC Security: A Paradigm Shift
Saha, D., Tarek, S., Yahyaei, K., Saha, S. K., Zhou, J., Tehranipoor, M. M., & Farahmandi, F. (2024) · IEEE Access · doi:10.1109/access.2024.3427369 · Cited by 128
Formal Verification of Circuits
Drechsler, R. (2000) · Springer eBooks · doi:10.1007/978-1-4757-3184-2 · Cited by 44
Self-citationUnlocking Hardware Security Assurance: The Potential of LLMsPreprint
Meng, X., Srivastava, A., Arunachalam, A., Ray, A., Silva, P. H., Psiakis, R., Makris, Y., & Basu, K. (2023) · arXiv (Cornell University) · doi:10.48550/arxiv.2308.11042 · Cited by 43
Research works printed but not linked: 6
- Kande, 2023, Llm-assisted generation of hardware assertions, arXiv preprint
- Orenes-Vera, 2023, From rtl to sva: Lim-assisted generation of formal verification testbenches, arXiv preprint
- Sun, 2023, Towards improving verification productivity with circuit-aware translation of natural language to systemverilog assertions
- Ahmad, 2023, Fixing hardware security bugs with large language models, arXiv preprint
- Zhang, 2023, LIm4dv: Using large language models for hardware test stimuli generation, arXiv preprint
- Brglez, 1985, A neutral netlist of 10 combinational benchmark circuits and a targeted translator in fortran
Cited by
VeriPlan: Integrating Formal Verification and LLMs into End-User Planning
Lee, C. P., Porfirio, D., Wang, X. J., Zhao, K. C., & Mutlu, B. (2025) · Proceedings of the 2025 CHI Conference on Human Factors in Computing Systems · doi:10.1145/3706598.3714113 · Cited by 21
Domain-Adapted LLMs for VLSI Design and Verification: A Case Study on Formal Verification
Liu, M., Kang, M., Hamad, G. B., Suhaib, S. M., & Ren, H. M. (2024) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts60656.2024.10538589 · Cited by 25
From Bugs to Fixes: HDL Bug Identification and Patching using LLMs and RAG
Qayyum, K., Hassan, M., Ahmadi-Pour, S., Jha, C. K., & Drechsler, R. (2024) · IEEE LLM Aided Design Workshop (LAD) · doi:10.1109/lad62341.2024.10691874 · Cited by 15
Self-citationFVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware
Kang, M., Liu, M., Hamad, G. B., Suhaib, S. M., & Ren, H. M. (2025) · Design, Automation, and Test in Europe · doi:10.23919/date64628.2025.10992720 · Cited by 14
A survey on large language models driven meta-optimizers for automated intelligent optimization
Zheng, Y., Zhang, L., Li, K., Wang, R., Li, W., Zhang, T., Zhang, Q., & Jin, Y. (2026) · Artificial Intelligence Review · doi:10.1007/s10462-025-11470-w · Cited by 14
Metadata
- Authors
- Hassan, M., Ahmadi-Pour, S., Qayyum, K., Jha, C. K., & Drechsler, R.
- Affiliations
- University of Bremen (DE)
- German Research Centre for Artificial Intelligence (DE)
- Venue
- 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE)
- Publisher
- IEEE
- Published
- 2024-03-25
- Pages
- 1-2
- OpenAlex
- W4401567960
- Cited by
- 43
- References
- 11
- Citations by year
- 2026: 13 · 2025: 21 · 2024: 9
- FWCI
- 27.95
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- Design, Automation, and Test in Europe (publishedVersion)
- Funders
- BMBF (01IW22002)
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
- Physical Sciences › Computer Science › Hardware and Architecture › Embedded Systems Design Techniques
- Keywords
- mutation testing, invariant generation, hardware verification, GPT-4, interrupt controller, ISCAS85 benchmarks
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
How to cite
Cite CoChat for the checks on this page, and the paper for its own findings.
- This page
- CoChat. (2026). Citation check: LLM-Guided Formal Verification Coupled with Mutation Testing. https://app.cochat.ai/papers/10.23919/date58400.2024.10546729
- The paper
- Hassan, M., Ahmadi-Pour, S., Qayyum, K., Jha, C. K., & Drechsler, R. (2024). LLM-Guided Formal Verification Coupled with Mutation Testing. 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE). https://doi.org/10.23919/date58400.2024.10546729
