Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Guangyu Hu, Chen Chen, Xiaofeng Zhou, Jiaxi Zhang, Wei Zhang, Hongce Zhang

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.

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

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.

Paper Structure

This paper contains 18 sections, 5 equations, 7 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Property Directed Reachability (PDR/IC3)
  4. Graph Neural Networks
  5. Methodology: Circuit-Aware PDR Solver Configuration
  6. Overview of AutoPDR
  7. Parameter Space Filtering
  8. Circuit Feature Extraction and Graph Representation
  9. Graph Representation Preprocessing via Cone of Influence
  10. Static Feature Extraction
  11. Learning Circuit-Aware PDR Solver Configuration
  12. Training Data Selection
  13. Empirical Evaluation of GNN Architecture
  14. Rank-Aware Hybrid Loss Function
  15. Experiments
  16. ...and 3 more sections

Figures (7)

  • Figure 1: Overview of AutoPDR.
  • Figure 2: Feature Extraction.
  • Figure 3: Memory consumption of parallel execution of PDR engines for a small and a large verification problem. The pink line represents the small case 6s0 with 157 state bits from the HWMCC13 benchmark. The blue line represents ILA_Flute_SUB_problem with 174263 state bits from the HWMCC24 benchmark.
  • Figure 4: Distribution of COI reduction percentages across 225 benchmarks from HWMCC'13.
  • Figure 5: Distribution of COI execution times across the same 225 benchmarks.
  • ...and 2 more figures