Certificate-Aware Property-Directed Reachability

TL;DR

CAPDR is a certificate-aware extension of Property-Directed Reachability that improves runtime, certificate size, and reproducibility for hardware safety verification, with formal guarantees and competitive results.

Contribution

We introduce CAPDR, a novel certificate-aware PDR variant that balances verification speed, certificate size, and reproducibility while maintaining trustworthiness.

Findings

CAPDR solves six more instances than the baseline on hardware benchmarks.

Median certificate size proxy decreases by 24.6%.

Median checker time decreases by 49%.

Abstract

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.