# AutoSVA: Democratizing Formal Verification of RTL Module Interactions

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

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Apr 2021.

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

- [Revisiting VerilogEval: A Year of Improvements in Large-Language Models for Hardware Code Generation](https://mlsanity.com/paper/2408.11053/) (2024)
- [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)
- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)
- [FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures](https://mlsanity.com/paper/2510.15906/) (2025)
- [HardSecBench: Benchmarking the Security Awareness of LLMs for Hardware Code Generation](https://mlsanity.com/paper/2601.13864/) (2026)
- [Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting](https://mlsanity.com/paper/2411.15442/) (2024)
- [VerilogLAVD: LLM-Aided Rule Generation for Vulnerability Detection in Verilog](https://mlsanity.com/paper/2508.13092/) (2025)
- [Principle-Guided Verilog Optimization: IP-Safe Knowledge Transfer via Local-Cloud Collaboration](https://mlsanity.com/paper/2508.05675/) (2025)
- [STELLAR: Structure-guided LLM Assertion Retrieval and Generation for Formal Verification](https://mlsanity.com/paper/2601.19903/) (2025)
- [HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification](https://mlsanity.com/paper/2606.13706/) (2026)
- [Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement](https://mlsanity.com/paper/2608.18482/) (2026)

## Abstract (arXiv)

Modern SoC design relies on the ability to separately verify IP blocks relative to their own specifications. Formal verification (FV) using SystemVerilog Assertions (SVA) is an effective method to exhaustively verify blocks at unit-level. Unfortunately, FV has a steep learning curve and requires engineering effort that discourages hardware designers from using it during RTL module development. We propose AutoSVA, a framework to automatically generate FV testbenches that verify liveness and safety of control logic involved in module interactions. We demonstrate AutoSVA's effectiveness and efficiency on deadlock-critical modules of widely-used open-source hardware projects.