一句话：提出 AIGROW，用运行时反馈生成小而难的问题，诊断硬件模型检测器性能差异并改进 CAR 检测器。
模型检测在硬件领域取得显著成功，很大程度上依赖于大量复杂优化与精细的实现细节；随着工具演化，诊断性能差异以理解这些因素的相互作用变得愈发重要，但现有能暴露差异的问题往往规模过大、难以人工审视，诊断价值有限。本文提出 AIGROW——一个硬件模型检测问题生成框架，并报告了用其生成的问题诊断模型检测器性能差异的经验。AIGROW 采用反馈引导的过程，基于运行时信息对问题不断演化，选择性保留对目标检测器变得更具挑战性的问题；随后在算法相近的硬件模型检测器上评估这些问题，从而暴露性能差异。实验表明，AIGROW 生成的问题比现有生成器小 100 倍以上，却仍能揭示显著的性能差异。基于这些诊断，作者对 CAR 系检测器做出了具体改进：发现其探索策略中的结构性低效、解决了 18 个此前无法解决的 HWMCC'24 问题，并在若干案例中将运行时间从小时级降至分钟级。
Model checking has achieved remarkable success in the hardware domain, largely due to the accumulation of intricate optimizations and finely tuned implementation details. As tools evolve, diagnosing performance differences to better understand the interplay of these factors has become increasingly important. Yet existing problems that reveal such differences are often too large for meaningful inspection, limiting their diagnostic value.To address the problem, this paper proposes AIGROW, a framework for generating hardware model checking problems, and introduces our experience on diagnosing performance differences in model checkers with the generated problems. AIGROW uses a feedback-guided process that evolves problems based on runtime information, selectively retaining those that become more difficult for a target checker. Performance differences are then revealed by evaluating these problems across hardware model checkers that have similar algorithms.Our evaluation demonstrates that AIGROW generates problems that are more than 100 times smaller than those produced by existing generators, while still revealing substantial performance differences. Diagnosing the performance differences has led to concrete improvements in CAR-based checkers: (1) uncovering structural inefficiencies in their exploration strategies, (2) solving 18 previously unsolvable HWMCC’24 problems, and (3) reducing runtime from hours to minutes in several cases.
DOI 原文 ·
@inproceedings{paperbot9480,
title = {Diagnosing Performance Differences in Model Checkers via Runtime-Guided Problem Generation},
author = {Yibo Dong and Yicong Xu and Wenjing Deng and Yu Chen and Xiaoyu Zhang and Jianwen Li and Chengyu Zhang and Geguang Pu},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00019}
}