EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
This work provides a novel method for generating diverse and challenging hardware model checking benchmarks, which is crucial for the rigorous evaluation and development of new verification techniques for hardware designers and researchers.
This paper addresses the lack of high-quality hardware model checking benchmarks by introducing EvolveGen, a framework that uses reinforcement learning (RL) and high-level synthesis (HLS) to generate benchmarks. The RL agent learns to construct computation graphs, which are then compiled into functionally equivalent but structurally distinct hardware designs, creating challenging model checking instances that expose solver weaknesses.
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.