Property-Directed Reachability (PDR/IC3) is a standard workhorse for hardware safety verification, but most implementations are tuned primarily for time-to-answer and treat the produced invariant or counterexample as a secondary byproduct. In certified workflows, including recent hardware model checking competition rules, the certificate becomes a deliverable whose size, independent checking time, and reproducibility directly affect end-to-end cost. We present CAPDR, a certificate-aware variant of PDR that targets a joint objective over runtime, certificate size, and checker time, while keeping learning outside the trusted computing base. CAPDR exposes a small set of PDR choice points (blocker generalization, obligation ordering, clause pushing, and optional extensions) to a learned ranking policy, but preserves trust by design: every state-changing action is guarded by the same SAT checks as standard PDR, and a SAFE/UNSAFE claim is reported only after an independent checker validates the emitted invariant or trace. We formalize certificate-centric metrics and a replay log that records nondeterministic choices for artifact-grade reproducibility. On the 2024 Hardware Model Checking Competition bit-level safety benchmarks, CAPDR solves six more instances than the baseline. Over each configuration's checker-accepted solved set, the median certificate-size proxy decreases by 24.6% and the median checker time by 49%. Post-fixpoint invariant minimization yields further reductions.

翻译：属性导向可达性（PDR/IC3）是硬件安全性验证的标准工具，但大多数实现主要针对求解时间进行优化，而将生成的不变量或反例视为次要副产品。在包含近期硬件模型检测竞赛规则的认证流程中，证书成为可交付物，其大小、独立检查时间及可复现性直接决定端到端成本。我们提出CAPDR——一种面向证书的PDR变体，旨在联合优化运行时、证书大小与检查器时间，同时将学习过程排除在可信计算基之外。CAPDR将少量PDR决策点（阻塞泛化、义务排序、子句传播及可选扩展）暴露给学习型排序策略，但通过设计保持可信性：每个状态变更操作均经与标准PDR相同的SAT检查守卫，且仅在独立检查器验证所生成的不变量或反例轨迹后，才报告安全/不安全声明。我们形式化定义了面向证书的度量指标与重放日志，该日志记录非确定性选择以实现人工制品级复现性。在2024年硬件模型检测竞赛的位级安全基准测试中，CAPDR比基线多解决6个实例。在各配置检查器接受的求解集合中，证书大小代理中位数降低24.6%，检查器中位数时间降低49%。经不动点后不变量最小化处理，这些指标进一步优化。