Property Directed Reachability (PDR) is a powerful algorithm for formal verification of hardware and software systems, but its performance is highly sensitive to parameter configurations. Manual parameter tuning is time-consuming and requires domain expertise, while traditional automated parameter tuning frameworks are not well-suited for time-sensitive verification tasks like PDR. This paper presents a circuit-aware solver configuration framework that employs graph learning for intelligent heuristic selection in PDR-based verification. Our approach combines graph representations with static circuit features to predict optimal PDR solving configurations for specific circuits. We incorporate expert prior knowledge through constraint-based parameter filtering to eliminate invalid and inefficient configurations and reduce 78% search space. Our feature extraction pipeline captures structural, functional, and connectivity characteristics of circuit topology and component patterns. Experimental evaluation on a comprehensive benchmark suite demonstrates significant performance improvements compared to default configurations and commonly-used settings. The system successfully identifies circuit-specific parameter patterns and automatically selects the most suitable solving strategies based on circuit characteristics, making it a practical tool for automated formal verification workflows.

翻译：性质导向可达性（PDR）是一种用于硬件与软件系统形式化验证的强大算法，但其性能对参数配置高度敏感。手动参数调优既耗时又需领域专业知识，而传统自动化参数调优框架难以适配PDR等对时间敏感的验证任务。本文提出一种电路感知的求解器配置框架，采用图学习为基于PDR的验证智能选择启发式策略。该方法结合图表示与静态电路特征，预测特定电路的最优PDR求解配置。我们通过基于约束的参数过滤融入专家先验知识，剔除无效与低效配置，将搜索空间缩减78%。特征提取流程捕捉了电路拓扑结构与元件组件的结构、功能及连通性特征。基于综合基准测试集的实验表明，与默认配置及常用设置相比，该方法实现了显著的性能提升。该系统能识别电路特定参数模式，并依据电路特征自动选择最优求解策略，从而成为自动化形式化验证流程的实用工具。