可以通过降低约束的复杂度来优化Formal的执行效率吗？

我们可以通过降低约束的复杂度来优化Formal的执行效率，但是这个主要是通过减少Formal验证空间来实现的，很容易出现过约，导致bug遗漏。

简化断言以优化Formal形式分析的主要挑战是：

由于DUT一般是比较复杂的，所以工程师们都倾向于使用长而复杂的，甚至单行断言来精确地编码DUT的期望行为。但是对于Formal形式分析而言，断言应该尽可能简单，断言所涉及的时序逻辑深度应该尽可能短，这样才能更快地完成证明。

断言简化的关键在于将你需要验证的复杂行为“分解”为最基本的行为元素，注意分解前后的断言一定要是等价的。

“相信”Formal形式工具能够合理安排这些浅逻辑深度断言的证明，下面是一个简单的例子示意：假设你有一个错误指示信号“error”，它的生成逻辑如下

assign error = err1 | err2;

其中“err1”和“err2”用于检测两种不同的错误场景。下面的原始的断言：断言error永远不会发生。

当其中“err1”或者“err2”后面的逻辑锥（COI）电路很大时，我们可能没有办法完成这个断言的证明。我们可以分解原始的断言，分别验证“err1“和“err2”。

如果“err1的逻辑锥比较小，“err2”的逻辑锥比较大，我们可能首先比较快地完成“err1”的断言证明，后面再针对性地优化“err2”的证明。

同样，对于下面这个例子：

我们也可以对复杂断言做简化，简化前后的断言版本是等价的，但是Formal形式分析的效果会好很多。

因为对于Formal工具而言，逻辑锥小的断言更容易完成证明，并且如果已经完成了一个简单断言验证之后，Formal工具会利用这个断言验证的结果去证明其他的断言。

审核编辑：刘清