Scholarlink

The advancement of hardware model checking is critically dependent on high-quality benchmarks. However, the community faces a significant benchmark gap: existing benchmark suites are limited in number, primarily provided at representations like BTOR2 without access to the originating register-transfer-level (RTL) designs, and skewed toward extreme difficulty levels, where instances are either trivial or intractable. These limitations not only impede the rigorous evaluation of new verification techniques but also encourage the overfitting of solver heuristics to a narrow set of problems. To address this challenge, we introduce EvolveGen, a novel framework that generates hardware model checking benchmarks by combining reinforcement learning (RL) with high-level synthesis (HLS). Our approach operates at an algorithmic level of abstraction, where an RL agent learns to construct computation graphs. By compiling these graphs with different synthesis directives, we generate pairs of functionally equivalent but structurally distinct hardware designs, thereby inducing challenging model checking instances. The solver’s execution time serves as a reward signal, guiding the agent to autonomously discover and generate “small-but-hard” instances that target solver-specific weaknesses. Our experiments show that EvolveGen efficiently creates a diverse benchmark set in various standard formats (e.g., AIGER, BTOR2), effectively revealing performance bottlenecks in state-of-the-art model checkers.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Guangyu Hu,
  • Xiaofeng Zhou,
  • Wei Zhang,
  • Hongce Zhang

摘要

The advancement of hardware model checking is critically dependent on high-quality benchmarks. However, the community faces a significant benchmark gap: existing benchmark suites are limited in number, primarily provided at representations like BTOR2 without access to the originating register-transfer-level (RTL) designs, and skewed toward extreme difficulty levels, where instances are either trivial or intractable. These limitations not only impede the rigorous evaluation of new verification techniques but also encourage the overfitting of solver heuristics to a narrow set of problems. To address this challenge, we introduce EvolveGen, a novel framework that generates hardware model checking benchmarks by combining reinforcement learning (RL) with high-level synthesis (HLS). Our approach operates at an algorithmic level of abstraction, where an RL agent learns to construct computation graphs. By compiling these graphs with different synthesis directives, we generate pairs of functionally equivalent but structurally distinct hardware designs, thereby inducing challenging model checking instances. The solver’s execution time serves as a reward signal, guiding the agent to autonomously discover and generate “small-but-hard” instances that target solver-specific weaknesses. Our experiments show that EvolveGen efficiently creates a diverse benchmark set in various standard formats (e.g., AIGER, BTOR2), effectively revealing performance bottlenecks in state-of-the-art model checkers.