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
Automated Hardware Logic Obfuscation Framework Using GPT
Latibari, B. S., Ghimire, S., Chowdhury, M. A., Nazari, N., Gubbi, K. I., Homayoun, H., Sasan, A., & Salehi, S. (2024) · IEEE Dallas Circuits and Systems Conference (DCAS) · doi:10.1109/dcas61159.2024.10539877 · Cited by 11
IoT systems testing: Taxonomy, empirical findings, and recommendations
Minani, J. B., Fellah, Y. E., Sabir, F., Moha, N., Guéhéneuc, Y., Kuradusenge, M., & Masuda, T. (2025) · Journal of Systems and Software · doi:10.1016/j.jss.2025.112408 · Cited by 13
Zhang, C., You, Y., Wang, N., Park, J., & Zhang, L. (2025) · IEEE Journal on Emerging and Selected Topics in Circuits and Systems · doi:10.1109/jetcas.2025.3575272 · Cited by 13
LLMs for Hardware Security: Boon or Bane?
Kande, R., Gohil, V., DeLorenzo, M. C., Chen, C., & Rajendran, J. (2024) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts60656.2024.10538871 · Cited by 12
Late Breaking Results: LLM-assisted Automated Incremental Proof Generation for Hardware Verification
Qayyum, K., Hassan, M., Ahmadi-Pour, S., Jha, C. K., & Drechsler, R. (2024) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/3649329.3663498 · Cited by 8
Self-citationNavigating SoC Security Landscape on LLM-Guided Paths
Paria, S., Dasgupta, A., & Bhunia, S. (2024) · ACM Great Lakes Symposium on VLSI (GLSVLSI) · doi:10.1145/3649476.3660393 · Cited by 7
Leveraging Large Language Models for the Automated Documentation of Hardware Designs
Fernando, S., Kunzelmann, R., Lopera, D. S., Halabi, J. A., & Ecker, W. (2024) · Mediterranean Conference on Embedded Computing (MECO) · doi:10.1109/meco62516.2024.10577923 · Cited by 7
Towards Automated Verification of IP and COTS: Leveraging LLMs in Pre- and Post-Silicon Stages
Paria, S., Dasgupta, A., & Bhunia, S. (2025) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts65138.2025.11022781 · Cited by 8
LASSO: LLM-Aided Security Property Generation for Assertion-based SoC Verification
Ankireddy, D. R., Paria, S., Dasgupta, A., Ray, S., & Bhunia, S. (2025) · ACM/IEEE Workshop on Machine Learning for CAD (MLCAD) · doi:10.1109/mlcad65511.2025.11189178 · Cited by 7
LLMs for Hardware Verification: Frameworks, Techniques, and Future Directions
Qayyum, K., Ahmadi-Pour, S., Jha, C. K., Hassan, M., & Drechsler, R. (2024) · Proceedings - Asian Test Symposium/Proceedings · doi:10.1109/ats64447.2024.10915476 · Cited by 6
Self-citationBridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification
Ramani, K., Tawosi, V., Alamir, S., & Borrajo, D. (2025) · IEEE/ACM International Conference on Automated Software Engineering Workshops (ASEW) · doi:10.1109/asew67777.2025.00018 · Cited by 5
Towards LLM-Assisted HDL Generation and Verification
Amin, R. A., Lincoln, M. G. R., & Obermaisser, R. (2025) · Mediterranean Conference on Embedded Computing (MECO) · doi:10.1109/meco66322.2025.11049176 · Cited by 4
Revolution or Hype? Seeking the Limits of Large Models in Hardware Design
Xu, Q., Stok, L., Drechsler, R., Wang, X., Zhang, G. L., & Markov, I. L. (2025) · doi:10.1109/iccad66269.2025.11240750 · Cited by 4
Self-citationiConPAL: LLM-guided Policy Authoring Assistant for Configuring IoT Defenses
Alam, M. M., Zhang, S., Rodriguez, E., Nafis, A. J., & Hoque, E. (2024) · IEEE Secure Development Conference (SecDev) · doi:10.1109/secdev61143.2024.00014 · Cited by 3
LISA: LLM Informed Systemverilog Assertion generation with RAG and Chain-of-Thought
Paul, S., Banerjee, A., Ghosh, S., Surendran, S., & Gajavelly, R. K. (2025) · IEEE Computer Society Annual Symposium on VLSI · doi:10.1109/isvlsi65124.2025.11130226 · Cited by 3
FV-PAL: Scalable Formal Verification through Partitioning and LLM-Guided Property Generation
Paria, S., Dasgupta, A., Ankireddy, D. R., Chakraborty, P., & Bhunia, S. (2025) · IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD) · doi:10.1109/iccd65941.2025.00114 · Cited by 3
Prompt. Verify. Repeat. LLMs in the Hardware Verification Cycle
Hassan, M., Nadeem, M., Qayyum, K., Jha, C. K., & Drechsler, R. (2025) · IEEE International Conference on Omni-layer Intelligent Systems (COINS) · doi:10.1109/coins65080.2025.11125767 · Cited by 3
Self-citationGiabbanelli, P. J., Beverley, J., Dávid, I., & Tolk, A. (2025) · SSRN Electronic Journal · doi:10.2139/ssrn.5365069 · Cited by 4
OpenAssert: Towards Secure Assertion Generation using Large Language Models
Menon, A., Miftah, S. S., Srivastava, A., Kundu, S., Kundu, S., Raha, A., Banerjee, S., Mathaikutty, D. A., & Basu, K. (2025) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts65138.2025.11022798 · Cited by 2
LogicCraft: LLM-Assisted Optimization of Netlist to Layout for Complex Custom Standard Cell Designs
Lin, M., Bui, D.-H., Wang, C., Lu, W., Tang, R., Zhang, Q., Zhang, Y., Zhao, J. P., Tran, X., & Li, Y. (2025) · IEEE International Conference on Artificial Intelligence Circuits and Systems (AICAS) · doi:10.1109/aicas64808.2025.11173139 · Cited by 2
Hou, Z., Duan, Z., Yang, M., Wu, M., & Yang, S. (2025) · IEEE International Conference on Software Quality, Reliability and Security (QRS) · doi:10.1109/qrs65678.2025.00015 · Cited by 1
Harnessing the Power of LLMs for Enhancing Hardware Security
Paria, S., & Bhunia, S. (2026) · SN Computer Science · doi:10.1007/s42979-026-04799-8 · Cited by 3
Giabbanelli, P. J., Beverley, J. R., Dávid, I., & Tolk, A. (2025) · Winter Simulation Conference · doi:10.1109/wsc68292.2025.11338852 · Cited by 1
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
LLM-assisted Performance Estimation of Embedded Software on RISC-V Processors
Zhang, W., Hassan, M. U., & Drechsler, R. (2025) · IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS) · doi:10.1109/ddecs63720.2025.11006767
Self-citationFirefly: Shedding Light on Verification Gaps using LLM-Powered Mutation Testing
Skakov, B., Abduraimov, S., Nurman, O., & Kabylkas, N. (2025) · ACM/IEEE Workshop on Machine Learning for CAD (MLCAD) · doi:10.1109/mlcad65511.2025.11189125
109PwnPilot: could an adversary be pair programming with our most trusted software engineers?
Horne, D. (2025) · De Gruyter eBooks · doi:10.1515/9783111436548-006
Transforming FPGA Learning and Research with LLM-Integrated Collaborative Platforms
Amin, R. A., Wiese, V., Weber, C., & Obermaisser, R. (2026) · Learning and analytics in intelligent systems · doi:10.1007/978-3-032-09058-4_10
Automatic SystemVerilog Assertion Generation: Challenges and Opportunities
Afsharmazayejani, R., Pearce, H. A., & Tan, B. (2025) · Conference proceedings - Canadian Conference on Electrical and Computer Engineering · doi:10.1109/ccece64018.2025.11364438
Opportunities and Risks of Generative AI in Model-Based Engineering of Railway Systems
Flammini, F., Nocente, A., Bernardeschi, C., & Vittorini, V. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-12484-5_6
SuperSAGA: A Supervisor-Subordinate Agentic workflow for the Generation of Assertions
Paul, S., Banerjee, A., Ghosh, S., Surendran, S., & Gajavelly, R. K. (2026) · Asia and South Pacific Design Automation Conference (ASP-DAC) · doi:10.1109/asp-dac66049.2026.11420235
Semantic-Guided Test Generation using Fine-Tuned LLMs for Validation of Hardware Accelerators
Andrews, E., Jayasena, A., & Mishra, P. (2026) · International Symposium on Quality Electronic Design (ISQED) · doi:10.1109/isqed69900.2026.11534681
Enabling Digital Transformation in Aerospace: Automated Model Based Engineering
Lalchandani, T., Purushothaman, K., Jeppu, Y., Kumar, S. H. V., & Natarajan, A. (2026) · SAE technical papers on CD-ROM/SAE technical paper series · doi:10.4271/2026-26-0722
FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification
Wan, L. J., Ho, C.-T., Bai, Y., Yu, C., Chen, D., & Ren, H. M. (2026) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts69484.2026.11563220 · Cited by 2
From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation
Mashnoor, N., Kamali, H., & Azar, K. Z. (2026) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts69484.2026.11563398
Zhang, J., Huang, Y., Chen, J., & Liu, M. (2026) · IEEE International Symposium on Circuits and Systems proceedings · doi:10.1109/iscas66217.2026.11563038
Automation of Polynomial Formal Verification using Large Language Models
Müller, L., Qayyum, K., Hugo, N., Hassan, M., & Drechsler, R. (2026) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts69484.2026.11563380
Self-citationEffect of Natural Language Descriptions on VHDL Code Generation in Fine-Tuned Large Language Models
Elsayed, M., Amin, R. A., & Obermaisser, R. (2026) · International Symposium ELMAR (ELMAR) · doi:10.1109/elmar71231.2026.11712191
Towards Reliable LLM-Assisted Verification Artifact Generation in EDA
Qayyum, K., Ain, Q. U., Hassan, M., Afnan, A., & Drechsler, R. (2026) · IEEE International Conference on Omni-layer Intelligent Systems (COINS) · doi:10.1109/coins69995.2026.11715594
Self-citation
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
