SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop

TL;DR

SpecLoop is an innovative framework that combines large language models and formal verification to generate accurate RTL specifications through an iterative feedback process, improving correctness and consistency.

Contribution

It introduces a novel agentic framework that integrates formal verification feedback into RTL specification generation, enhancing fidelity over prior LLM-based methods.

Findings

Formal verification feedback significantly improves specification accuracy.

Iterative refinement leads to more consistent RTL-to-specification mappings.

The framework outperforms LLM-only baselines in correctness and robustness.

Abstract

RTL implementations frequently lack up-to-date or consistent specifications, making comprehension, maintenance, and verification costly and error-prone. While prior work has explored generating specifications from RTL using large language models (LLMs), ensuring that the generated documents faithfully capture design intent remains a major challenge. We present SpecLoop, an agentic framework for RTL-to-specification generation with a formal-verification-driven iterative feedback loop. SpecLoop first generates candidate specifications and then reconstructs RTL from these specifications; it uses formal equivalence checking tools between the reconstructed RTL and the original design to validate functional consistency. When mismatches are detected, counterexamples are fed back to iteratively refine the specifications until equivalence is proven or no further progress can be made. Experiments across multiple LLMs and RTL benchmarks show that incorporating formal verification feedback substantially improves specification correctness and robustness over LLM-only baselines, demonstrating the effectiveness of verification-guided specification generation.