Interpretable and Verifiable Hardware Generation with LLM-Driven Stepwise Refinement
For hardware engineers, this framework provides a trustworthy approach to leveraging LLMs for RTL generation by ensuring correctness through formal verification.
The paper proposes a hardware generation framework that combines LLMs with formal methods to produce correct-by-construction RTL code, addressing the hallucination problem in LLM-based code generation. Experimental results show the framework effectively generates correct RTL designs.
Large language models (LLMs) have achieved remarkable success in software development. However, they are susceptible to hallucinations, meaning that they can introduce subtle semantic and logical errors. Due to the high stakes in chip design and manufacturing, hardware engineers are still reluctant to rely on LLMs for register-transfer level (RTL) generation. In this paper, we propose a hardware generation framework that combines the creativity and broad knowledge of LLMs with the explainability and mathematical rigor of formal methods. Specifically, we devise a set of transformation rules that cover various design decisions and hardware features. By iteratively applying these rules, an LLM agent can convert a design specification into an RTL program with guaranteed correctness. Experimental results demonstrate the effectiveness and efficiency of the framework.