Formal验证三要素解析：Input、Object与Output的作用

Formal三要素：input(输入) + object(对象) + output(输出)。Formal有点像上帝，我们把input和object灌进formal，formal会给出个output来指示结果是否正确。

Object：是我们要证明的对象，通常是DUT；

Input：是我们给的输入，通常是assert和assume，assert是预期的行为，assume是假定的行为；

Output：是formal依据input和object推导出的结果。Output通常有三种结果：1. 证明成功；2. 证明失败，并给出反例波形；3. 还没有证明完成，可能需要更多的时间；

由于Formal本身性质，证明的cycle时间越长，所需要的计算量是指数级增长的，在超过formal可验证时间之外的bug是无法检查出来。有两种方法可以降低：1. 减少FF，2. 减低bug检查的cycle。

在formal验证中，需要注意不要over constraint，否则会漏检测bug，宁愿constraint放宽点，这样会覆盖的范围更广点，虽然可能会导致误报一些counter examples，但验证更全面的，这有点类似simulation。为了检查formal有没有过约束，一方面可以assert和assume互换交叉验证，另一方面可以利用formal工具生成的覆盖率来分析所灌入的激励是否过约束和check的点是否都覆盖，这一点也类似simulation。

formal和simulation的一大区别是：formal只要用户没有说不能做，它都全部遍历；simulation是遍历用户规定的行为，虽然这些行为是用户自己random出来的，但也算是用户规定的范围。

formal和simulation都需要关注不要出现over constraint，否则导致验证空间的缩小；

formal和simulation也都需要关注覆盖率，来调整constraint；formal和simulation的完备性目前只能通过人和工具一块分析尽可能达到的。人根据经验想好各种可能得场景和激励，工具可以生成覆盖率来查看DUT验证的是否充分。