Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Guangyu Hu, Xiaofeng Zhou, Wei Zhang, Hongce Zhang

TL;DR

EvolveGen is introduced, a framework for generating hardware model checking benchmarks by combining reinforcement learning (RL) with high-level synthesis (HLS) and effectively reveals performance bottlenecks in state-of-the-art model checkers.

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.

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

TL;DR

EvolveGen is introduced, a framework for generating hardware model checking benchmarks by combining reinforcement learning (RL) with high-level synthesis (HLS) and effectively reveals performance bottlenecks in state-of-the-art model checkers.

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.
Paper Structure (27 sections, 1 equation, 8 figures, 3 tables, 1 algorithm)

This paper contains 27 sections, 1 equation, 8 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related work.
  3. Contributions.
  4. Structure of the Paper.
  5. Preliminaries
  6. Hardware Model Checking.
  7. High-Level Synthesis.
  8. Reinforcement Learning.
  9. Motivation
  10. Analysis of Existing Benchmarks.
  11. A Motivating Example.
  12. The EvolveGen Framework
  13. Computation Graph Representation
  14. Benchmark Synthesis from Computation Graphs
  15. Frontend RL-Guided Graph Generation
  16. ...and 12 more sections

Figures (8)

  • 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.
  • Figure 5: The backend workflow: synthesizing computation graphs to hardware designs.
  • ...and 3 more figures