Search papers, labs, and topics across Lattice.
The paper introduces EvolveGen, a reinforcement learning framework that generates hardware model checking benchmarks by evolving computation graphs at an algorithmic level and compiling them using high-level synthesis. This approach addresses the benchmark gap in hardware model checking by creating diverse, small-but-hard instances that expose solver-specific weaknesses. Experiments demonstrate that EvolveGen effectively generates benchmarks in standard formats (AIGER and BTOR2) and reveals performance bottlenecks in state-of-the-art model checkers.
Tired of benchmarks that are either too easy or impossible? EvolveGen uses RL to automatically generate "goldilocks" hardware model checking problems that expose the weaknesses of your solver.
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.
