EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning

TL;DR

EvolveGen leverages reinforcement learning and high-level synthesis to generate diverse, challenging hardware model checking benchmarks, addressing existing limitations and exposing solver weaknesses for improved verification evaluation.

Contribution

This paper introduces EvolveGen, a novel RL-based framework that synthesizes structurally diverse and challenging hardware benchmarks at the algorithmic level.

Findings

EvolveGen efficiently generates diverse benchmark sets.

The generated benchmarks reveal performance bottlenecks in state-of-the-art model checkers.

The approach produces benchmarks in standard formats like AIGER and BTOR2.

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.