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%。特征提取流水线捕获了电路拓扑与组件模式的结构、功能和连接特性。在综合基准测试集上的实验评估表明，与默认配置和常用设置相比，性能显著提升。该系统成功识别出电路特定的参数模式，并能根据电路特性自动选择最合适的求解策略，从而成为自动化形式化验证工作流程中的实用工具。