Model checking is an automatic formal verification technique that is widely used in hardware verification. The state-of-the-art complete model-checking techniques, based on IC3/PDR and its general variant CAR, are based on computing symbolically sets of under - and over-approximating state sets (called frames) with multiple calls to a SAT solver. The performance of those techniques is sensitive to the order of the assumptions with which the SAT solver is invoked, because it affects the unsatisfiable cores - which the solver emits when the formula is unsatisfiable - that crucially affect the search process. This observation was previously published in [15], where two partial assumption ordering strategies, intersection and rotation were suggested (partial in the sense that they determine the order of only a subset of the literals). In this paper we extend and improve these strategies based on an analysis of the reason for their effectiveness. We prove that intersection is effective because of what we call locality of the cores, and our improved strategy is based on this observation. We conclude our paper with an extensive empirical evaluation of the various ordering techniques. One of our strategies, Hybrid-CAR, which switches between strategies at runtime, not only outperforms other, fixed ordering strategies, but also outperforms other state-of-the-art bug-finding algorithms such as ABC-BMC.

翻译：模型检测是一种广泛应用于硬件验证的自动形式化验证技术。当前最先进的完备模型检测技术，基于IC3/PDR及其通用变体CAR，通过多次调用SAT求解器来计算符号化的欠近似与过近似状态集（称为框架）。这些技术的性能对调用SAT求解器时所使用假设的排序非常敏感，因为它会影响求解器在公式不可满足时输出的不可满足核，而这对搜索过程至关重要。这一观察先前发表于文献[15]，其中提出了两种部分假设排序策略：交集策略与轮换策略（所谓“部分”是指它们仅确定部分文字子集的顺序）。本文基于对其有效性原因的分析，扩展并改进了这些策略。我们证明交集策略之所以有效，是因为我们称之为核的局部性特性，而我们的改进策略正是基于这一观察。最后，我们对多种排序技术进行了广泛的实证评估。我们提出的动态切换策略的混合方法Hybrid-CAR，不仅优于其他固定排序策略，也超越了如ABC-BMC等其他最先进的错误查找算法。