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

Guangyu Hu; Xiaofeng Zhou; Wei Zhang; Hongce Zhang

cs.ARFeb 26, 2026

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

Authors: Guangyu Hu, Xiaofeng Zhou, Wei Zhang, Hongce Zhang

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

Panel of Figure 1 — Figure 1: Analysis of the HWMCC’24 benchmark suite. (a) The difficulty spectrum is highly polarized, with a scarcity of mid-difficulty instances (600s-3600s). Solving time is measured on Pono. (b) Benchmark difficulty is strongly correlated with circuit size, indicating scale-driven difficulty.

Figure 2: Two functionally equivalent C++ implementations of a multiply-accumulate loop, differing only by HLS pragmas. Version A is pipelined, while Version B is fully unrolled, leading to vastly different hardware implementations.

Figure 3: The overall workflow of our proposed EvolveGen framework.

Figure 4: Examples of different type of nodes in a computation graph with the corresponding code snippet, where c is a constant.

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

Table 1: Node types and their attributes.

Figure 5: The backend workflow: synthesizing computation graphs to hardware designs.

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.

Table 2: Key features used by the model checking difficulty predictor model.

Panel of Figure 6 — Figure 6: Maximum solving time of derived model checking problems over time

Solver	Metric	AIGen	AIGFuzz	FuzzBtor	EvolveGen
ABC-PDR	Size	720179	26851	162548	15279
	Time	17.03	243.38	3600.00	3600.00
	$\overline{QR}$	1.00 $\times 10^{-4}$	3.84 $\times 10^{-2}$	9.36 $\times 10^{-2}$	1.00
IC3Ref	Size	719888	29079	194439	16329
	Time	17.78	294.58	3.73	3600.00
	$\overline{QR}$	1.12 $\times 10^{-4}$	4.59 $\times 10^{-2}$	8.73 $\times 10^{-5}$	1.00

Table 3: Comparison of different tools across various model checkers (for each model checker and each solver, we perform 24-hour generation and calculate the average of 10 most challenging cases, and

\overline{QR}

is calculated by the ratio of the average solving time and the average benchmark size, and normalized ). Timeouts are calculated as 3600s .

Panel of Figure 7 — Figure 7: Distribution of $QR$ , for baseline tools, i.e., AIGen, AIGFuzz, and FuzzBtor, we pick the top 100 slowest generated benchmarks, and for EvolveGen , we use the whole generated benchmark suite.

Figure 8: Performance comparison between rIC3 and Pono under the generated benchmark suite.

Synthetic Benchmark Generation

Synthetic benchmark generation creates controlled, verifiable evaluation tasks and datasets to test models across diverse settings.

See all 287 papers

RTL-BenchLS: A Large-Scale Benchmark for RTL Reasoning and Generation with Large Language Models
Jun 8, 2026Jing Wang, Shang Liu, Wenji Fang +3LLM Evaluation Benchmark Design
Hong Kong University of Science and Technology
CovR: Coverage-Aware Hardware Verification via Reasoning-Guided Reinforcement Learning
Sep 15, 2026Manar Abdelatty, Maryam Nouh, Sherief RedaAutomated Test Generation Reinforcement Learning with Verifiable Rewards
School of Engineering Brown University Providence, RI, USA
CHORUS: Complementary Experts for High-Coverage Testbench Stimulus Generation
Aug 10, 2026Hejia Zhang, Sheng Lu, Zhongming Yu +3RL for Code Generation Automated Test Generation
1UC San Diego · 2Georgia Institute of Technology · 3NVIDIA

Jun 8, 2026J/K move · Enter open · S save

RTL-BenchLS: A Large-Scale Benchmark for RTL Reasoning and Generation with Large Language Models

Jing Wang, Shang Liu, Wenji Fang, Yuchao Wu+2

Hong Kong University of Science and Technology

LLM Evaluation Benchmark Design Code Generation RTL Code Generation

Open paper AskPDF arXiv

LLM-based RTL generation and reasoning is a promising direction for hardware design automation. High-quality benchmarks are critical infrastructure for tracking progress in this direction. However, existing RTL benchmarks face inherent limitations in both scale and task scope. The designs they cover are typically small and simple, and the tasks focus almost entirely on specification-to-RTL generation. Frontier models' performance already saturates on the existing benchmarks. Scaling these benchmarks up is fundamentally difficult because aligned labels are required for benchmarking, such as specifications and testbenches. Such aligned high-quality data are rarely available for real-world designs. We introduce RTL-BenchLS, a large-scale benchmark addressing both limitations above. It contains over 10,000 formally verified Verilog designs, covering substantially larger and more complex designs than existing benchmarks. Beyond specification-to-RTL generation, we propose three novel tasks that jointly evaluate reasoning and generation: round-trip reasoning, masked-content reasoning, and repository-issue reasoning. The first two are self-supervised, which directly resolves the scaling bottleneck. All tasks are verified through formal equivalence checking without any manual testbenches. We evaluate eight LLMs on RTL-BenchLS. Even the best model reaches only 23% on natural-language round-trip reasoning, 28% on masked-content reasoning, and 12% on repository-issue fixing. RTL-BenchLS is substantially more challenging than existing benchmarks. It leaves ample room for future improvement and offers guidance for developing LLM-based methods for hardware design.

Abstract

Synthetic Benchmark Generation

Explore similar work

RTL-BenchLS: A Large-Scale Benchmark for RTL Reasoning and Generation with Large Language Models

CovR: Coverage-Aware Hardware Verification via Reasoning-Guided Reinforcement Learning

CHORUS: Complementary Experts for High-Coverage Testbench Stimulus Generation