英特尔关于正式思维扩展的主题演讲

由柏拉图重新发布

关注： 0

Synopsys 在 SolvNet 网站上发布了英特尔显卡公司 Theo Drane 博士的精彩演讲。主题是数据路径等效性检查。听起来可能像是又一个 Synopsys VC 正式 DPV 认可，但无论如何你都应该观看它。这是关于正式的使用和注意事项的一次拓展思维的讨论，它将带您超越常规的用户指南，进入更迷人的领域。

英特尔正式主题演讲

理智理解与样本测试

各种形式的测试驱动仿真在验证设计规范或实现的正确性方面都非常出色，并且通常是不可替代的。上手也很容易。只需编写一个测试程序并开始模拟即可。但这种简单性的另一面是我们不需要充分了解我们正在测试什么才能开始。我们说服自己，我们已经仔细阅读了规范并理解了所有的极端情况，但并不需要太多复杂的复杂性来压倒我们的理解。

正式鼓励您深入了解功能（至少如果您想提供有价值的结果）。在上面的示例中，一个简单的问题（z 是否可以全为 1）无法在模拟器上演示十亿个周期的示例。这并不奇怪，因为这是一个极端的极端情况。正式测试在 188 秒内提供了一个具体且非常不明显的示例，并且可以在稍短的时间内证明这是唯一的此类情况。

好的，正式的可以做到动态测试无法做到的事情，但更重要的是，您学到了模拟器可能永远不会告诉您的东西。只有一种可能的情况会发生这种情况。形式化帮助您在智力层面上更好地理解设计，而不仅仅是有限测试用例集的概率总结。

规格问题

Theo 的下一个例子是基于一个虫子自动售货机（之所以这么叫是因为当你按下一个按钮时，你就会得到一个虫子）。这看起来像是一个非常简单的 C 到 RTL 等价检查问题，左边是 C 模型，右边是 RTL 模型。 Theo 在其早期的正式生涯中遇到的一个意外是，C 模型中的右移行为并未在 C 标准中完全定义，尽管 gcc 的行为是合理的。然而，DPV 会抱怨与 RTL 的比较不匹配，这是理所应当的。依赖未定义的行为是一件危险的事情。

正式作为虫子自动售货机

C 和 RTL 之间的规格比较还存在其他危险，尤其是位宽方面。中间信号中进位位的截断或丢失（上面#3）就是很好的例子。这些是规格问题吗？也许规范和实现选择之间存在灰色地带。

超越等价性检查

DPV 的主要目的似乎是检查 C 或 RTL 引用与 RTL 实现之间的等效性。但这种需求相对较少，而且这种技术还有其他有用的方法可以应用，如果有点开箱即用的话。首先是实现世界中的经典 - 我进行了更改，修复了错误 - 结果是否引入了任何新错误？有点像添加时钟门控后的 SEQ 检查。在某些情况下，块输出中的可达性分析可能是另一个有用的应用。

不仅仅是等价性检查