Large language models improve hardware verification with semantic guidance
Enhancing Word-Level Property Directed Reachability with LLM-Driven Semantic Guidance
Hardware Architecture
Summary
Checking hardware designs to make sure they work as expected is hard because detailed bit-level methods lose sight of the bigger picture. The authors developed a way to help formal verification tools by using large language models to suggest helpful hints based on the design’s meaning. Their method improves how quickly and effectively verification runs on complex hardware like pipelines and memory controllers. Tests showed their approach solves more verification tasks and speeds up checking compared to previous methods.
What this means in practice
- •For hardware verification engineers: Accelerate formal verification of complex datapath and pipeline hardware designs by using LLM-generated semantic guidance within word-level PDR.
- •For embedded systems developers: Improve verification efficiency for hardware-software interfaces by integrating LLM-guided proofs in hardware model checking workflows.
Authors
Guangyu Hu, Mingkai Miao, Zhiyuan Yan, Xiaofeng Zhou, Wei Zhang, Hongce Zhang
Abstract
Property Directed Reachability (PDR) is a prominent algorithm for hardware formal verification. However, bit-level PDR often struggles with datapath-heavy designs because bit-blasting obscures high-level semantics. While word-level PDR addresses this by reasoning over bit-vector and array theories, its performance remains bottlenecked by discovering proof-relevant word-level relations. We propose LLM4PDR, a framework leveraging Large Language Models (LLMs) to guide word-level PDR search through three mechanisms: (1) Predicate Generation, extracting state relationships as candidate predicates during inductive generalization; (2) Clause Generation, producing candidate frame lemmas to accelerate convergence after formal validation; and (3) Assertion Generation, synthesizing helper assertions that strengthen the target property under counterexample-guided refinement. We implement LLM4PDR in the Pono model checker and evaluate it on arithmetic micro-benchmarks, HLS-generated pipelines, open-source RTL components, and hardware model checking competition (HWMCC) instances. Results show LLM-generated guidance improves both solved instances and runtime on datapath-heavy and control-plus-datapath designs. The strongest configuration solves 28 of 33 arithmetic benchmarks, compared to 13 for vanilla Pono and 11 for AVR. On HLS pipelines and open-source RTL, different modes provide complementary speedups: clause guidance is effective for deep pipelines and predicate guidance for bus and memory-controller designs. On HWMCC benchmarks, benefits are instance-dependent, demonstrating notable speedups and timeout avoidance on hard cases. These results suggest that LLM-generated, verifier-checked semantic hints can serve as a practical complement to conventional word-level PDR.