BDD与SAT合作的验证方法：工业实验与性能提升

本文主要探讨了在工业环境下如何有效地结合二元决策图（BDDs）和布尔可满足性（SAT）求解器进行目标包围和动态抽象的验证方法。BDDs和SAT作为两种强大的验证技术，各自在处理复杂逻辑结构和解决大规模布尔表达式方面具有优势。作者提出的创新方法旨在充分利用这两种工具的优点，以提高验证效率。 首先，作者介绍了一个核心思想，即在验证过程中，从BDDs出发，当问题规模尚能控制时，继续进行BDD的验证。一旦问题变得过于复杂，便切换到SAT求解器，同时保留BDD阶段的工作成果。这种策略通过"目标扩大"来实现，即通过广度优先的高密度动态抽象技术，对初始和目标状态集进行排序BDD操作，从而收集欠近似可达的状态集合。这种方法有助于扩展验证范围，增强SAT验证的效果。 在实际应用中，作者将这一方法应用于英特尔BOONUVERIFIER，通过对标准基准如ISCAS'89、ISCAS'89-附录和VIS套件，以及工业基准如IBM官方验证基准库的实验，结果显示了显著的优势。相比于最先进的技术，当在相同的深度下执行验证时，该方法能够将CPU时间减少高达5倍。另一方面，如果在给定的时间限制内验证，他们可以将验证深度提升30%，这意味着在效率上取得了显著的提升。 关键词：“不变量检查”，“布尔可满足性求解器（SAT）”，“二元决策图（BDDs）”，“目标包围”体现了文章的核心关注点，即通过集成BDDs和SAT的特性，优化工业设计验证过程，提高正确性和效率。这种方法的提出对于推动现代设计验证技术的发展具有重要意义，尤其是在确保复杂系统设计的正确性和提前发现问题方面。