AutoPDR: Circuit-Aware Solver Configuration Prediction for Hardware Model Checking

TL;DR

AutoPDR introduces a circuit-aware, graph learning-based framework to predict optimal solver configurations for hardware model checking, significantly improving performance over default settings.

Contribution

It presents a novel graph learning approach that combines circuit features and expert knowledge to automate and optimize PDR solver configuration selection.

Findings

Achieves 78% reduction in search space through constraint-based filtering.

Demonstrates significant performance improvements on a comprehensive benchmark suite.

Automatically identifies circuit-specific parameter patterns for better solver strategies.

Abstract

Property Directed Reachability (PDR) is a powerful algorithm for formal verification of hardware and software systems, but its performance is highly sensitive to parameter configurations. Manual parameter tuning is time-consuming and requires domain expertise, while traditional automated parameter tuning frameworks are not well-suited for time-sensitive verification tasks like PDR. This paper presents a circuit-aware solver configuration framework that employs graph learning for intelligent heuristic selection in PDR-based verification. Our approach combines graph representations with static circuit features to predict optimal PDR solving configurations for specific circuits. We incorporate expert prior knowledge through constraint-based parameter filtering to eliminate invalid and inefficient configurations and reduce 78% search space. Our feature extraction pipeline captures structural, functional, and connectivity characteristics of circuit topology and component patterns. Experimental evaluation on a comprehensive benchmark suite demonstrates significant performance improvements compared to default configurations and commonly-used settings. The system successfully identifies circuit-specific parameter patterns and automatically selects the most suitable solving strategies based on circuit characteristics, making it a practical tool for automated formal verification workflows.