인증 인지형 속성 지향 도달 가능성 (Certificate-Aware Property-Directed Reachability)

속성 지향 도달 가능성 (Property-Directed Reachability, PDR/IC3)은 하드웨어 안전성 검증 (hardware safety verification)을 위한 표준적인 핵심 도구이지만, 대부분의 구현체는 주로 답변 시간 (time-to-answer)에 맞춰 조정되어 있으며 생성된 불변량 (invariant) 또는 반례 (counterexample)를 부차적인 부산물로 취급합니다. 최근의 하드웨어 모델 체킹 (hardware model checking) 경진대회 규칙을 포함한 인증 워크플로우 (certified workflows)에서는, 인증서 (certificate)가 그 크기, 독립 검증 시간, 그리고 재현성 (reproducibility)이 엔드 투 엔드 비용 (end-to-end cost)에 직접적인 영향을 미치는 결과물 (deliverable)이 됩니다. 본 논문에서는 실행 시간, 인증서 크기, 그리고 검증기 시간 (checker time)에 대한 공동 목표를 대상으로 하면서, 학습 과정을 신뢰 컴퓨팅 기반 (trusted computing base) 외부로 유지하는 PDR의 인증 인지형 변형인 CAPDR을 제시합니다. CAPDR은 소수의 PDR 선택 지점 (blocker generalization, obligation ordering, clause pushing 및 선택적 확장)을 학습된 랭킹 정책 (learned ranking policy)에 노출시키지만, 설계 단계부터 신뢰성을 보존합니다. 즉, 모든 상태 변경 동작은 표준 PDR과 동일한 SAT 체크에 의해 보호되며, SAFE/UNSAFE 주장은 독립적인 검증기가 생성된 불변량 또는 트레이스 (trace)를 검증한 후에만 보고됩니다. 우리는 인증서 중심의 지표 (certificate-centric metrics)와 산출물 수준의 재현성을 위해 비결정론적 선택 (nondeterministic choices)을 기록하는 리플레이 로그 (replay log)를 공식화합니다. 2024 Hardware Model Checking Competition의 비트 수준 안전성 벤치마크 (bit-level safety benchmarks)에서, CAPDR은 베이스라인보다 6개의 인스턴스를 더 해결했습니다. 각 구성의 검증기 승인 해결 집합 (checker-accepted solved set)에 대해, 중앙값 인증서 크기 프록시 (median certificate-size proxy)는 24.6% 감소하였고, 중앙값 검증기 시간 (median checker time)은 49% 감소했습니다. 고정점 이후의 불변량 최소화 (Post-fixpoint invariant minimization)를 통해 추가적인 감소를 달성했습니다.