Synopsys 中的不确定断言 VC 正式
Inconclusive Assertion in Synopsys VC Formal
2 个问题 -
- 在基于断言的形式验证中，如果我得到一个不确定的断言，那么处理该断言或收敛它的各种方法是什么？
- 开发参考 rtl 并编写断言以在每个活动时钟边沿比较参考 rtl 输出与 DUT 输出是否是正确的方法？它会增加有效的状态空间并因此增加复杂性，运行 时间吗？
如果有人可以为基于断言的形式验证提供一些很好的参考 material，这也会有所帮助，因为我在这个主题上找不到太多 articles/papers。
我已经得到了我自己的问题的答案，所以我在这里发布。
不确定的断言是形式验证的自然组成部分。因此，如果您有 "Required Proof Bound Depth"，验证签字仍然是可能的。 （它类似于基于模拟的验证中的覆盖范围，如果您已获得所需的覆盖范围数字，您仍然可以在其中签署验证）。要获得 "Required Proof Bound Depth"，必须联系设计团队。
有界证明深度 > 所需证明深度 => 相当于完全证明
有界证明可能有多种原因。
- 设计的状态 Space and/or 断言
- 设计的复杂性and/or断言
- 工具选项（工作量运行 时间记忆约束算法）
所以你的方法应该是"Required Proof Bound".
现在要获得必需的证明绑定，有多种选择。
- Tool/Resource 选项（努力水平，运行 时间，内存限制）
- 状态 Space 和复杂性选项
- Modify/Add 约束条件
- 黑拳
- 切点
- 修改断言
- 更改参数化设计的参数值
- 基于模拟的重置状态
- 指导证明
- 抽象
仍然，无法保证通过这种方法获得所需的证明绑定。因此，通常不使用独立的形式验证，而是使用它作为基于模拟的验证的补充
是的，比较参考模型和 DUT 输出会增加复杂性，因此如果需要，应尽量少使用参考模型。
2 个问题 -
- 在基于断言的形式验证中，如果我得到一个不确定的断言，那么处理该断言或收敛它的各种方法是什么？
- 开发参考 rtl 并编写断言以在每个活动时钟边沿比较参考 rtl 输出与 DUT 输出是否是正确的方法？它会增加有效的状态空间并因此增加复杂性，运行 时间吗？
如果有人可以为基于断言的形式验证提供一些很好的参考 material，这也会有所帮助，因为我在这个主题上找不到太多 articles/papers。
我已经得到了我自己的问题的答案，所以我在这里发布。
不确定的断言是形式验证的自然组成部分。因此，如果您有 "Required Proof Bound Depth"，验证签字仍然是可能的。 （它类似于基于模拟的验证中的覆盖范围，如果您已获得所需的覆盖范围数字，您仍然可以在其中签署验证）。要获得 "Required Proof Bound Depth"，必须联系设计团队。
有界证明深度 > 所需证明深度 => 相当于完全证明
有界证明可能有多种原因。
- 设计的状态 Space and/or 断言
- 设计的复杂性and/or断言
- 工具选项（工作量运行 时间记忆约束算法）
所以你的方法应该是"Required Proof Bound".
现在要获得必需的证明绑定，有多种选择。
- Tool/Resource 选项（努力水平，运行 时间，内存限制）
- 状态 Space 和复杂性选项
- Modify/Add 约束条件
- 黑拳
- 切点
- 修改断言
- 更改参数化设计的参数值
- 基于模拟的重置状态
- 指导证明
- 抽象
仍然，无法保证通过这种方法获得所需的证明绑定。因此，通常不使用独立的形式验证，而是使用它作为基于模拟的验证的补充
是的，比较参考模型和 DUT 输出会增加复杂性，因此如果需要，应尽量少使用参考模型。