formal-verification - Synopsys VC Formal 中的不确定断言

Question

2 个问题 -

1. 在基于断言的形式验证中，如果我得到一个不确定的断言，那么处理该断言或收敛它的各种方法是什么？
2. 开发参考 rtl 并编写断言来比较参考 rtl 输出与每个有效时钟沿上的 DUT 输出是否是正确的方法？它会增加有效的状态空间并因此增加复杂性和运行时间吗？

如果有人可以为基于断言的形式验证提供一些很好的参考材料，这也会很有帮助，因为我找不到太多关于这个主题的文章/论文。

Answer 1

我已经得到了我自己问题的答案，所以我在这里发布它。

非结论性断言是形式验证的自然部分。因此，如果您已获得“必需的证明绑定深度”，则验证签名仍然是可能的。（它类似于基于模拟的验证中的覆盖范围，如果您获得了所需的覆盖范围编号，您仍然可以签署验证）。要获得“Required Proof Bound Depth”，必须联系设计团队。

有界证明深度 > 所需证明深度 => 等效于完全证明

有界证明可能是由于多种原因。

• 设计和/或断言的状态空间
• 设计和/或断言的复杂性
• 工具选项（工作量级运行时内存约束算法）

所以你的方法应该是获得“必需的证明约束”。

现在要获得必需的证明绑定，有多种选择。

• 工具/资源选项（工作量、运行时间、内存限制）
• 状态空间和复杂性选项
  • 修改/添加约束
  • 黑盒
  • 切入点
  • 修改断言
  • 更改参数化设计的参数值
  • 基于模拟的复位状态
  • 引导证明
  • 抽象

尽管如此，通过这种方法无法保证获得所需的证明约束。所以通常情况下，不使用独立的形式验证，而是使用它，而不是作为基于模拟的验证的补充

是的，比较参考模型和 DUT 输出会增加复杂性，因此如果需要，应尽量少使用参考模型。