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.

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