Search papers, labs, and topics across Lattice.
SpecLoop is introduced, an agentic framework that leverages LLMs to generate specifications from RTL code and iteratively refines them using formal verification. The framework reconstructs RTL from the generated specifications and uses equivalence checking against the original RTL, feeding counterexamples back to the LLM for refinement. Results show that this verification-guided feedback loop significantly improves the correctness and robustness of generated specifications compared to LLM-only approaches.
Formal verification can guide LLMs to produce RTL specifications that are significantly more accurate and robust than those generated by LLMs alone.
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.
