Presentation
Late Breaking Results: LLM-assisted Automated Incremental Proof Generation for Hardware Verification
DescriptionIn 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 and a Dadda Tree multiplier demonstrate that LLMs enhance the efficiency and accuracy of hardware verification.
Event Type
Late Breaking Results Poster
TimeWednesday, June 266:00pm - 7:00pm PDT
LocationLevel 2 Lobby