扩展CTG泛化与IC3中泛化策略的动态调整
形式语言与自动机理论
2025-01-10 v1 计算机科学中的逻辑
摘要
IC3算法广泛应用于硬件形式化验证，其中泛化是关键步骤。标准泛化通过丢弃文字来扩展立方体，以包含更多不可达状态。CTG方法通过在丢弃文字失败时阻止泛化反例（CTG）来增强泛化。本文扩展了CTG方法（EXCTG），在泛化上投入更多努力。如果阻止CTG失败，EXCTG尝试阻止其前驱，以期获得更好的泛化。虽然CTG和EXCTG提供了更好的泛化结果，但也带来了更高的计算开销。使用静态策略在泛化质量和计算开销之间找到适当平衡具有挑战性。我们提出DynAMic，一种根据阻止状态的难度动态调整泛化策略的方法，从而在不牺牲效率的情况下提高可扩展性。综合评估表明，与CTG泛化相比，EXCTG和DynAMic分别多解决了8个和25个案例，实现了显著的可扩展性提升。
引用
@article{arxiv.2501.02480,
title = {Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3},
author = {Yuheng Su and Qiusong Yang and Yiwei Ci and Ziyu Huang},
journal= {arXiv preprint arXiv:2501.02480},
year = {2025}
}