[经验]

列举一个memory controller的示例

2022-8-31 14:56:02

2797

在formal验证过程中，很多时候我们针对所负责模块做了非常完备的覆盖率和断言检查，但是涉及到接口的约束往往会引入过约，即

我们对所验证模块的约束没有完整地传给上游模块，作为上游模块的输出assert。

下面举一个memory controller的示例，这个memory controller接收请求，并对特定内存地址执行某些操作。

一开始断言证明各种规格属性时验证工程师会定位出各种反例（counterexamples），然后会依次添加合理的约束。

其中的一个反例就是 某个操作（opcode）需要多个周期完成，在这个期间地址发生了变化，导致规格属性证明错误。 Formal验证工程师发现之后，就会很自然地约束在某个操作发起和完成期间地址不允许变化。

结果，一旦添加了这个assume约束，所有的memory controller规格属性都得到了证明，从而这个Formal验证工程师就很有信心地觉得自己完成了FPV工作。

然而，实际上，上游模块传下来的地址并不一定在整个多周期的操作期间保持不变，自以为下游模块会在操作的第一拍进行锁存，可事实上并没有。

这个接口行为并没有从上游完整地传递给下游，而下游的这个约束也没有完整地传递给上游模块。

如果这个模块仅仅做Formal sign off，必然会将bug遗漏到更高层次的验证环境、甚至是硅后。这个时候再去争吵是上游模块设计/验证人员的锅，还是下游模块设计/验证人员的锅对于项目来说都没有意义了。

因此，基于这个“操作期间地址不会发生变化”的约束前提下的任何规格断言证明都是无效证明。

所以，针对formal证明过程中的任何形式的约束都要进行各种形式的人工检视或者EDA simulation 互补验证保证。

原作者：验证师布林

只看该作者 淘帖0 举报

快速回复 返回顶部 返回列表

关注微信公众号

电子发烧友网

电子发烧友论坛

站长推荐 /7