EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
Organizations: The Hong Kong University of Science and Technology · The Hong Kong University of Science and Technology (Guangzhou)
Abstract
Progress in hardware model checking depends critically on high-quality benchmarks. However, the community faces a significant benchmark gap: existing suites are limited in number, often distributed only in representations such as BTOR2 without access to the originating register-transfer-level (RTL) designs, and biased toward extreme difficulty where instances are either trivial or intractable. These limitations hinder rigorous evaluation of new verification techniques and encourage overfitting of solver heuristics to a narrow set of problems. To address this, we introduce EvolveGen, a framework for generating hardware model checking benchmarks by combining reinforcement learning (RL) with high-level synthesis (HLS). Our approach operates at an algorithmic level of abstraction in which an RL agent learns to construct computation graphs. By compiling these graphs under different synthesis directives, we produce pairs of functionally equivalent but structurally distinct hardware designs, inducing challenging model checking instances. Solver runtime is used as the reward signal, enabling the agent to autonomously discover and generate small-but-hard instances that expose solver-specific weaknesses. Experiments show that EvolveGen efficiently creates a diverse benchmark set in standard formats (e.g., AIGER and BTOR2) and effectively reveals performance bottlenecks in state-of-the-art model checkers.
Figures & tables
| Node type | Attributes |
|---|---|
| OpNode | operation type, data width, data type, rounding mode, saturation mode, and the integer value bits count |
| LoopNode | whether pipelined, whether flattened, loop variable information (including starting index, ending index, and the step size), unrolling mode (unroll factor, whether fully unrolled) |
| BranchNode | the branch condition |
| DepNode | N/A |
| Category | Feature Class | Description and Rationale |
| Static | Size Metrics | Basic indicators of circuit scale (PI, flip-flop, AIG node counts). |
| Structural Complexity | Measures of functional units (MUX, XOR, adder counts). | |
| Topological Depth | Captures the longest path and overall circuit topology (max/avg depth). | |
| Sequential Connectivity | Quantifies dependencies between state elements (flop fanout statistics). | |
| Dynamic | PDR Proof Complexity | Internal statistics from a short PDR run (e.g., number of generated |
| clauses, proof obligations, and SAT solver calls) to gauge initial proof effort. |
| Solver | Metric | AIGen | AIGFuzz | FuzzBtor | EvolveGen |
|---|---|---|---|---|---|
| ABC-PDR | Size | 720179 | 26851 | 162548 | 15279 |
| Time | 17.03 | 243.38 | 3600.00 | 3600.00 | |
| 1.00 | 3.84 | 9.36 | 1.00 | ||
| IC3Ref | Size | 719888 | 29079 | 194439 | 16329 |
| Time | 17.78 | 294.58 | 3.73 | 3600.00 | |
| 1.12 | 4.59 | 8.73 | 1.00 |
Synthetic Benchmark Generation
Synthetic benchmark generation creates controlled, verifiable evaluation tasks and datasets to test models across diverse settings.
See all 287 papers