Certificate-Aware Property-Directed Reachability

Abstract

Property-Directed Reachability (PDR/IC3) is widely used for hardware safety verification. Most implementations optimize time-to-answer, but certified workflows also require compact, inexpensive-to-check, and reproducible certificates. We introduce CAPDR, whose ranker is fitted offline on a disjoint development corpus, frozen, and used only to order PDR-generated proposals on unseen instances to target solving time, certificate size, and checker time. The ranker remains outside the trusted computing base: it cannot bypass the SAT guards on blocker insertion and pushing; obligation scheduling remains fair, and every SAFE/UNSAFE claim requires independent checker acceptance. CAPDR also defines certificate-centric metrics and replay logs for artifact-grade reproducibility. On the 2024 Hardware Model Checking Competition bit-level safety benchmarks, CAPDR solves six more instances than the same PDR engine with ranking disabled. Across each configuration’s checker-accepted solved set, the medians of the certificate-size proxy and checker time decrease by 24.6% and 49%, respectively. After the same post-hoc minimizer is applied to paired SAFE outputs, CAPDR certificates still contain 16.3% fewer literals and have 38.5% lower checker time. Index Terms—Hardware model checking, property-directed reachability, proof-carrying verification, certificate checking, learning-guided heuristics