Reproduce “Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Ha Trung Tran
The authors present a multi-agent LLM system that repairs RTL bugs using formal counterexamples and checks repairs with k-induction. It generates properties from a specification, verifies them with an open-source backend, and uses assertions to guide RTL edits. In a six-module benchmark, the ALU repair passed in all five runs; the other five modules did not pass, limiting the result to feasibility.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.