# Using LLMs to Facilitate Formal Verification of RTL

arXiv: https://arxiv.org/abs/2309.09437 · HTML: https://mlsanity.com/paper/2309.09437/

## Key facts

- Cited by 18 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Sep 2023.

## Built on by (most cited first, 18 of 18)

- [LLM4EDA: Emerging Progress in Large Language Models for Electronic Design Automation](https://mlsanity.com/paper/2401.12224/) (2023)
- [LLM for SoC Security: A Paradigm Shift](https://mlsanity.com/paper/2310.06046/) (2023)
- [ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation](https://mlsanity.com/paper/2402.00093/) (2024)
- [AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation](https://mlsanity.com/paper/2406.18627/) (2024)
- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)
- [FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware](https://mlsanity.com/paper/2410.23299/) (2024)
- [New Solutions on LLM Acceleration, Optimization, and Application](https://mlsanity.com/paper/2406.10903/) (2024)
- [Are LLMs Any Good for High-Level Synthesis?](https://mlsanity.com/paper/2408.10428/) (2024)
- [Are LLMs Ready for Practical Adoption for Assertion Generation?](https://mlsanity.com/paper/2502.20633/) (2025)
- [Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting](https://mlsanity.com/paper/2411.15442/) (2024)
- [Can LLMs Make (Personalized) Access Control Decisions?](https://mlsanity.com/paper/2511.20284/) (2025)
- [Large Language Models (LLMs) for Electronic Design Automation (EDA)](https://mlsanity.com/paper/2508.20030/) (2025)
- [Semantic Consensus Decoding: Backdoor Defense for Verilog Code Generation](https://mlsanity.com/paper/2602.04195/) (2026)
- [VerilogLAVD: LLM-Aided Rule Generation for Vulnerability Detection in Verilog](https://mlsanity.com/paper/2508.13092/) (2025)
- [Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach](https://mlsanity.com/paper/2312.17353/) (2023)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)
- [GoGoTB: Agentic RTL Verification with Specification-Grounded Coverage Closure](https://mlsanity.com/paper/2607.26181/) (2026)
- [BEHAVE: Functional Behavior Modeling Enables Self-Improving Agents for Hardware Design and Verification](https://mlsanity.com/paper/2609.34785/) (2026)

## Abstract (arXiv)

Formal property verification (FPV) has existed for decades and has been shown to be effective at finding intricate RTL bugs. However, formal properties, such as those written as SystemVerilog Assertions (SVA), are time-consuming and error-prone to write, even for experienced users. Prior work has attempted to lighten this burden by raising the abstraction level so that SVA is generated from high-level specifications. However, this does not eliminate the manual effort of reasoning and writing about the detailed hardware behavior. Motivated by the increased need for FPV in the era of heterogeneous hardware and the advances in large language models (LLMs), we set out to explore whether LLMs can capture RTL behavior and generate correct SVA properties. First, we design an FPV-based evaluation framework that measures the correctness and completeness of SVA. Then, we evaluate GPT4 iteratively to craft the set of syntax and semantic rules needed to prompt it toward creating better SVA. We extend the open-source AutoSVA framework by integrating our improved GPT4-based flow to generate safety properties, in addition to facilitating their existing flow for liveness properties. Lastly, our use cases evaluate (1) the FPV coverage of GPT4-generated SVA on complex open-source RTL and (2) using generated SVA to prompt GPT4 to create RTL from scratch. Through these experiments, we find that GPT4 can generate correct SVA even for flawed RTL, without mirroring design errors. Particularly, it generated SVA that exposed a bug in the RISC-V CVA6 core that eluded the prior work's evaluation.