Certificate-Aware Property-Directed Reachability
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917502336892928 |
|---|---|
| author | Ferdowsi, Arman Kovacs, Laura |
| author_facet | Ferdowsi, Arman Kovacs, Laura |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_16472 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Certificate-Aware Property-Directed Reachability Ferdowsi, Arman Kovacs, Laura Logic in Computer Science Hardware Architecture 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. |
| title | Certificate-Aware Property-Directed Reachability |
| topic | Logic in Computer Science Hardware Architecture |
| url | https://arxiv.org/abs/2605.16472 |