在formal验证过程中，很多时候我们针对所负责模块做了非常完备的覆盖率和断言检查，但是涉及到接口的约束往往会引入过约，即
我们对所验证模块的约束没有完整地传给上游模块，作为上游模块的输出assert。
下面举一个memory controller的示例，这个memory controller接收请求，并对特定内存地址执行某些操作。
一开始断言证明各种规格属性时验证工程师会定位出各种反例（counterexamples），然后会依次添加合理的约束。
其中的一个反例就是某个操作（opcode）需要多个周期完成，在这个期间地址发生了变化，导致规格属性证明错误。Formal验证工程师发现之后，就会很自然地约束在某个操作发起和完成期间地址不允许变化。
结果，一旦添加了这个assume约束，所有的memory controller规格属性都得到了证明，从而这个Formal验证工程师就很有信心地觉得自己完成了FPV工作。
然而，实际上，上游模块传下来的地址并不一定在整个多周期的操作期间保持不变，自以为下游模块会在操作的第一拍进行锁存，可事实上并没有。
这个接口行为并没有从上游完整地传递给下游，而下游的这个约束也没有完整地传递给上游模块。
如果这个模块仅仅做Formal sign off，必然会将bug遗漏到更高层次的验证环境、甚至是硅后。这个时候再去争吵是上游模块设计/验证人员的锅，还是下游模块设计/验证人员的锅对于项目来说都没有意义了。
因此，基于这个“操作期间地址不会发生变化”的约束前提下的任何规格断言证明都是无效证明。
所以，针对formal证明过程中的任何形式的约束都要进行各种形式的人工检视或者EDA simulation 互补验证保证。
作者：验证师布林
来源：芯片验证工程师
推荐阅读
更多数字IC设计技术干货等请关注数字芯片实验室专栏。添加极术小姐姐（微信：aijishu20)微信可申请加入IC设计交流群。
