用语义聚类和搜索优化减少硬件验证中的冗余断言，提升仿真效率。
Arcane: An Assertion Reduction Framework through Semantic Clustering and MCTS-Guided Rule Exploring
- 通过两层聚类识别断言语义相似性，精准分类大量断言。
- 结合蒙特卡洛树搜索，找到最优断言精简规则序列，最多减少76.2%断言数。
- 保留完整形式化覆盖率与故障检测能力，适合芯片验证工程师使用。
断言驱动的硬件验证（ABV）对确保设计符合规格至关重要。然而，现有基于大模型的自动断言生成方法常产生大量冗余断言，严重降低仿真效率。本文提出Arcane框架，通过两级断言聚类实现大规模断言集的精确语义分类，并利用蒙特卡洛树搜索（MCTS）探索最优规则应用序列，实现高效断言精简。在Assertionbench [20] 上的实验表明，Arcane可将断言数量最多减少76.2%，同时完全保持形式化覆盖率和突变检测能力。进一步的仿真测试显示，仿真时间提速2.6倍至6.1倍。该框架已公开发布于 https://anonymous.4open.science/r/Arcane1-0A6F/。
原文摘要 · Abstract (English)
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/.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。