Saved in:
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.02895 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912939814944768 |
|---|---|
| author | Chang, Fu-Chieh Yang, Yu-Hsin Huang, Hung-Ming Hsu, Yun-Chia Lin, Yin-Yu Tsai, Ming-Fang Yang, Chun-Chih Wu, Pei-Yuan |
| author_facet | Chang, Fu-Chieh Yang, Yu-Hsin Huang, Hung-Ming Hsu, Yun-Chia Lin, Yin-Yu Tsai, Ming-Fang Yang, Chun-Chih Wu, Pei-Yuan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_02895 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop Chang, Fu-Chieh Yang, Yu-Hsin Huang, Hung-Ming Hsu, Yun-Chia Lin, Yin-Yu Tsai, Ming-Fang Yang, Chun-Chih Wu, Pei-Yuan Hardware Architecture Programming Languages 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. |
| title | SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop |
| topic | Hardware Architecture Programming Languages |
| url | https://arxiv.org/abs/2603.02895 |