发表机构
The Hong Kong University of Science and Technology; Hong Kong University of Science and Technology (Guangzhou)（香港科技大学; 香港科技大学（广州））
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对字级PDR在数据路径设计上的性能瓶颈，提出LLM4PDR框架，利用LLM生成谓词、子句和断言引导搜索，在多个基准上显著提升求解数量和运行时间。
AI 中文摘要
属性定向可达性（PDR）是硬件形式验证中的一种重要算法。然而，位级PDR在处理数据路径密集型设计时常常遇到困难，因为位爆破掩盖了高层语义。虽然字级PDR通过基于位向量和数组理论进行推理来解决这一问题，但其性能仍受限于发现与证明相关的字级关系。我们提出了LLM4PDR，一个利用大型语言模型（LLMs）通过三种机制引导字级PDR搜索的框架：（1）谓词生成，在归纳泛化过程中提取状态关系作为候选谓词；（2）子句生成，在形式验证后生成候选框架引理以加速收敛；（3）断言生成，在反例引导的细化过程中合成辅助断言以强化目标属性。我们在Pono模型检查器中实现了LLM4PDR，并在算术微基准、HLS生成的流水线、开源RTL组件以及硬件模型检查竞赛（HWMCC）实例上进行了评估。结果表明，LLM生成的引导在数据路径密集型和控制加数据路径型设计上提高了求解实例数量和运行时间。最强的配置解决了33个算术基准中的28个，而vanilla Pono为13个，AVR为11个。在HLS流水线和开源RTL上，不同模式提供了互补的加速：子句引导对深层流水线有效，谓词引导对总线和内存控制器设计有效。在HWMCC基准上，收益因实例而异，在困难案例上显示出显著的加速和超时避免。这些结果表明，LLM生成的、经过验证器检查的语义提示可以作为传统字级PDR的实用补充。
英文摘要
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.
Comments14 pages, 8 figures
