Assertion-based Verification (ABV) is essential for ensuring that hardware designs conform to their intended specifications. However, existing automated assertion-generation approaches, such as LLM-based frameworks, often generate large numbers of redundant assertions, which significantly degrade simulation efficiency. To mitigate the simulation overhead caused by redundant assertions, this paper proposes Arcane, an efficient assertion reduction framework. It integrates a two-tier assertion clustering approach for accurate semantic classification of large assertion sets, and employs Monte Carlo Tree Search (MCTS) to explore optimal rule-application sequences for efficient assertion reduction. The experimental results on Assertionbench [20] show that Arcane achieves a reduction of up to 76.2% in the assertion count while fully preserving formal coverage and mutation-detection ability. Further simulation studies demonstrate a speedup of 2.6x to 6.1x speedup in simulation time. The proposed framework is released at https://anonymous.4open.science/r/Arcane1-0A6F/.

翻译：基于断言的验证（ABV）对于确保硬件设计符合其预期规范至关重要。然而，现有的自动化断言生成方法（例如基于大语言模型的框架）往往产生大量冗余断言，这显著降低了仿真效率。为减轻冗余断言带来的仿真开销，本文提出Arcan——一种高效的断言约简框架。该框架融合了两级断言聚类方法以实现大规模断言集的精确语义分类，并采用蒙特卡洛树搜索（MCTS）探索最优规则应用序列以实现高效的断言约简。在Assertionbench [20]上的实验结果表明，Arcan在完全保持形式化覆盖率和突变检测能力的前提下，将断言数量最高减少76.2%。进一步的仿真研究显示，仿真时间实现了2.6倍至6.1倍的加速比。所提出的框架已发布于https://anonymous.4open.science/r/Arcane1-0A6F/。