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

📄 arXiv: 2602.22609v1 📥 PDF

作者: Guangyu Hu, Xiaofeng Zhou, Wei Zhang, Hongce Zhang

分类: cs.AR, cs.LG

发布日期: 2026-02-26

备注: 19 pages, 8 figures. Accepted by TACAS 2026

💡 一句话要点

EvolveGen：利用强化学习生成硬件模型检测算法级基准测试，提升验证效率。

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)

关键词: 硬件模型检测 强化学习 高级综合 基准测试生成 算法级 性能评估

📋 核心要点

  1. 现有硬件模型检测基准测试集数量少、RTL设计不可访问，且难度分布不均，限制了新验证技术的评估。
  2. EvolveGen结合强化学习与高级综合，在算法层面生成计算图，并编译为功能等效但结构不同的硬件设计。
  3. 实验表明，EvolveGen能高效生成多样化的基准测试集，并有效揭示现有模型检测器的性能瓶颈。

📝 摘要（中文）

硬件模型检测的进展严重依赖于高质量的基准测试。然而，当前领域面临着显著的基准测试差距：现有测试套件数量有限，通常仅以BTOR2等格式分发，无法访问原始寄存器传输级（RTL）设计，并且偏向于极端难度，实例要么过于简单，要么难以处理。这些限制阻碍了对新验证技术的严格评估，并鼓励求解器启发式算法过度拟合到狭窄的问题集。为了解决这个问题，我们引入了EvolveGen，一个通过将强化学习（RL）与高级综合（HLS）相结合来生成硬件模型检测基准的框架。我们的方法在算法抽象级别上运行，其中RL代理学习构建计算图。通过在不同的综合指令下编译这些图，我们生成功能等效但结构不同的硬件设计对，从而产生具有挑战性的模型检测实例。求解器运行时间被用作奖励信号，使代理能够自主地发现和生成暴露求解器特定弱点的小而难的实例。实验表明，EvolveGen有效地创建了标准格式（例如，AIGER和BTOR2）的多样化基准集，并有效地揭示了最先进模型检测器中的性能瓶颈。

🔬 方法详解

问题定义：硬件模型检测领域缺乏高质量的基准测试集。现有的基准测试集数量有限，通常以BTOR2等格式提供，无法访问原始的RTL设计。此外，这些基准测试集往往难度分布不均，要么过于简单，要么过于复杂，难以有效评估新的验证技术，容易导致求解器启发式算法的过拟合。

核心思路：EvolveGen的核心思路是利用强化学习（RL）自动生成具有挑战性的硬件模型检测基准测试。通过在算法级别上构建计算图，并使用高级综合（HLS）将其编译为功能等效但结构不同的硬件设计，从而创建具有挑战性的模型检测实例。使用求解器运行时间作为奖励信号，引导RL代理发现和生成能够暴露求解器弱点的“小而难”的实例。

技术框架：EvolveGen的整体框架包含以下几个主要模块：1) RL代理：负责学习生成计算图的策略。2) 计算图生成器：根据RL代理的输出生成计算图。3) 高级综合器（HLS）：将计算图编译为RTL硬件设计，并使用不同的综合指令生成功能等效但结构不同的设计。4) 模型检测器：用于验证生成的硬件设计，并提供运行时间作为RL代理的奖励信号。5) 基准测试集：存储生成的具有挑战性的模型检测实例。

关键创新：EvolveGen的关键创新在于将强化学习与高级综合相结合，实现了算法级别的硬件模型检测基准测试的自动生成。与传统的基准测试生成方法相比，EvolveGen能够自主地发现和生成能够暴露求解器弱点的“小而难”的实例，从而更有效地评估和改进模型检测器。

关键设计：RL代理使用策略梯度算法进行训练，奖励函数基于模型检测器的运行时间。计算图的结构和操作类型由RL代理控制。高级综合器使用不同的综合指令（例如，不同的资源约束、调度策略等）来生成功能等效但结构不同的硬件设计。生成的基准测试集以标准格式（例如，AIGER和BTOR2）存储，方便与其他工具集成。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，EvolveGen能够有效地生成多样化的基准测试集，并成功揭示了最先进模型检测器中的性能瓶颈。例如，EvolveGen生成的基准测试集能够显著增加某些模型检测器的运行时间，表明其能够有效地暴露求解器的弱点。生成的基准测试集以AIGER和BTOR2等标准格式提供，方便集成到现有的验证流程中。

🎯 应用场景

EvolveGen可用于硬件模型检测器的性能评估与优化，帮助发现求解器中的性能瓶颈。生成的基准测试集可用于训练和评估新的验证技术，提高硬件验证的效率和可靠性。此外，该方法还可应用于硬件安全漏洞的自动挖掘。

📄 摘要（原文）

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.