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

📄 arXiv: 2602.22609 📥 PDF

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

分类: cs.AR, cs.LG

发布日期: 2026-02-28

💡 一句话要点

EvolveGen：基于强化学习的硬件模型检测算法级基准生成框架

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

关键词: 硬件模型检测 强化学习 高级综合 基准生成 形式化验证

📋 核心要点

  1. 现有硬件模型检测基准数量有限，缺乏RTL设计，难度分布不均，限制了新验证技术的评估。
  2. EvolveGen利用强化学习生成计算图，通过高级综合生成功能等效但结构不同的硬件设计对，构成模型检测实例。
  3. 实验表明，EvolveGen能有效生成多样化的基准集，并揭示现有模型检测器的性能瓶颈。

📝 摘要（中文）

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

🔬 方法详解

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

核心思路：EvolveGen的核心思路是利用强化学习（RL）自动生成具有挑战性的硬件模型检测基准。通过在算法级别上进行操作，RL代理学习构建计算图，这些计算图随后通过高级综合（HLS）编译成硬件设计。通过使用不同的综合指令，可以生成功能等效但结构不同的硬件设计对，从而创建具有挑战性的模型检测实例。这种方法允许生成既小又难的实例，这些实例可以暴露求解器中的特定弱点。

技术框架：EvolveGen的整体框架包括以下几个主要模块：1) RL代理：负责学习生成计算图；2) 高级综合（HLS）：将计算图编译成硬件设计；3) 模型检测器：用于评估生成的硬件设计对的难度；4) 奖励函数：基于模型检测器的运行时间，用于训练RL代理。RL代理根据奖励信号不断调整其策略，以生成更具挑战性的基准测试。

关键创新：EvolveGen的关键创新在于它使用强化学习在算法级别上自动生成硬件模型检测基准。与手动创建或从现有设计中提取基准测试相比，这种方法可以生成更多样化和具有挑战性的实例。此外，通过使用求解器运行时间作为奖励信号，EvolveGen可以自主地发现和生成暴露求解器特定弱点的实例。这与以往依赖人工设计的基准测试方法有本质区别。

关键设计：EvolveGen的关键设计包括：1) RL代理的网络结构和训练算法；2) 高级综合工具的选择和配置；3) 奖励函数的定义，例如，可以使用求解器的运行时间或内存使用量作为奖励信号；4) 计算图的表示方法，例如，可以使用有向无环图（DAG）来表示计算图。这些设计细节会影响EvolveGen生成基准测试的质量和效率。

🖼️ 关键图片

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.