如何降低形式验证的复杂度？

当计数器和内存处于我们所需要证明断言的逻辑锥中，它们可能是Formal无法完成证明的根本原因。

因为形式分析算法很难适应非常大的状态空间，而计数器和存储器都会引入很多的状态空间和时序深度。针对这个问题，我们可以在不影响验证完备性的条件下减小计数器和存储器的大小或者用抽象模型替换。

Formal验证中优化大计数器的一种流行且有效的方法是将它们替换为小型的状态机模型（状态空间小），该模型仅考虑会触发设计操作的计数器临界值。例如，假设计数器的值“m”、“n-1”和“n”很关键。考虑以下状态机作为替代：

为了用这个抽象模型替换原始计数器，我们首先绕过真实设计的驱动逻辑（用cutpoint的方式“切割”原始计数器输出信号，使其变成一个自由随机变量，然后向其添加约束）

下面是一个计数器示例

这种办法主要还是用于bug-hunting，而且如果RTL中的其他部分实际就需要计数器延迟特定周期，那么这个优化方法就不适用了，所以说此时就没法用作formal full prove。