Late Breaking Results: LLM-assisted Automated Incremental Proof Generation for Hardware Verification
Khushboo Qayyum, Muhammad Hassan, Sallar Ahmadi-Pour, Chandan Kumar Jha, Rolf Drechsler · 2024
In this paper, we propose a methodology for hardware verification assisted by Large Language Models (LLMs) in the incremental proof generation process. First, an LLM identifies the basic module of the Design Under Verification (DUV), followed by expanding the proof scope as more modules are added. LLMs assist in defining and verifying invariants for each module using the Z3 solver, and in formulating integration properties at module interfaces. Our case studies on a Ripple Carry Adder (RCA) and a Dadda Tree Multiplier (DTM) demonstrate that LLMs enhance the efficiency and accuracy of hardware verification.