EvolveGen: 通过强化学习生成硬件模型检查基准的算法层面
EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
AI总结：
EvolveGen通过强化学习和高级合成生成多样化硬件模型检查基准，解决现有基准不足问题，揭示求解器弱点。
摘要：
硬件模型检查的进步严重依赖于高质量的基准测试。然而，社区面临显著的基准测试缺口：现有套件数量有限，往往仅以BTOR2等表示形式分布，而无法访问原始寄存器传输级（RTL）设计，并且偏向极端难度，实例要么是琐碎的要么是不可解的。这些限制阻碍了新验证技术的严格评估，并鼓励求解器启发式方法过度适应狭窄的问题集。为了解决这个问题，我们引入EvolveGen，一个通过结合强化学习（RL）和高级合成（HLS）生成硬件模型检查基准的框架。我们的方法在算法抽象级别上运行，在其中RL代理学习构建计算图。通过在不同的合成指令下编译这些图，我们生成功能等价但结构不同的硬件设计，从而产生具有挑战性的模型检查实例。求解器运行时间被用作奖励信号，使代理能够自主发现并生成小但难的实例，暴露求解器特定的弱点。实验表明，EvolveGen能够高效地生成标准格式（如AIGER和BTOR2）的多样化基准集，并有效揭示了最先进的模型检查器的性能瓶颈。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
