# Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 28 references that are in the map.
- First posted on arXiv 23 Nov 2024.

## Builds on (most cited first, 12 of 12)

- [Scaling Language Models: Methods, Analysis & Insights from Training Gopher](https://mlsanity.com/paper/2112.11446/) (2021)
- [VeriGen: A Large Language Model for Verilog Code Generation](https://mlsanity.com/paper/2308.00708/) (2023)
- [Software Testing with Large Language Models: Survey, Landscape, and Vision](https://mlsanity.com/paper/2307.07221/) (2023)
- [oLMpics -- On what Language Model Pre-training Captures](https://mlsanity.com/paper/1912.13283/) (2019)
- [Multi-hop Reading Comprehension through Question Decomposition and Rescoring](https://mlsanity.com/paper/1906.02916/) (2019)
- [Less Training, More Repairing Please: Revisiting Automated Program Repair via Zero-shot Learning](https://mlsanity.com/paper/2207.08281/) (2022)
- [A Syntax-Guided Edit Decoder for Neural Program Repair](https://mlsanity.com/paper/2106.08253/) (2021)
- [DAVE: Deriving Automatically Verilog from English](https://mlsanity.com/paper/2009.01026/) (2020)
- [(Security) Assertions by Large Language Models](https://mlsanity.com/paper/2306.14027/) (2023)
- [Using LLMs to Facilitate Formal Verification of RTL](https://mlsanity.com/paper/2309.09437/) (2023)
- [ITER: Iterative Neural Repair for Multi-Location Patches](https://mlsanity.com/paper/2304.12015/) (2023)
- [AutoSVA: Democratizing Formal Verification of RTL Module Interactions](https://mlsanity.com/paper/2104.04003/) (2021)

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

- [Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA](https://mlsanity.com/paper/2506.21569/) (2025)
- [ChatSVA: Bridging SVA Generation for Hardware Verification via Task-Specific LLMs](https://mlsanity.com/paper/2604.02811/) (2026)
- [VeriPilot: An LLM-Powered Verilog Debugging Framework](https://mlsanity.com/paper/2606.23759/) (2026)
- [A Survey on LLM-Integrated Hardware Design Verification](https://mlsanity.com/paper/2610.10580/) (2026)

## Abstract (arXiv)

Formal Property Verification (FPV), using SystemVerilog Assertions (SVA), is crucial for ensuring the completeness of design with respect to the specification. However, writing SVA is a laborious task and has a steep learning curve. In this work, we present a large language model (LLM) -based flow to automatically generate high-quality SVA from the design specification documents, named ToolName. We introduce a novel sub-task-focused fine-tuning approach that effectively addresses functionally incorrect assertions produced by baseline LLMs, leading to a remarkable 7.3-fold increase in the number of functionally correct assertions. Recognizing the prevalence of syntax and semantic errors, we also developed an iterative refinement method that enhances the LLM's initial outputs by systematically re-prompting it to correct identified issues. This process is further strengthened by a custom compiler that generates meaningful error messages, guiding the LLM towards improved accuracy. The experiments demonstrate a 26% increase in the number of assertions free from syntax errors using this approach, showcasing its potential to streamline the FPV process.