正式将取代模拟

有显著的心理变化在形式验证领域在过去几年。它不再是被认为是边缘技术,不再被认为是很难使用。事实上,它已成为一个必要的验证过程的一部分。

半导体工程坐下来与一个专家小组来找出是什么导致了这种变化,我们在未来可以期待从形式验证技术。参与小组皮特荷迪,在节奏敏锐的正式产品管理总监;盎司Levia,营销和业务发展副总裁碧玉设计自动化;在真正的意图Pranav莎,首席技术官;营销总监戴夫•Kelf OneSpin解决方案;首席执行官和Vigyan Singhal Oski技术。以下是摘录的讨论。

SE:这种变化的催化剂是什么?

Singhal:能力和方法是推动者。我们现在有工具可以扩展,人们已经学会了如何运用正式的分手问题。社区提出了必要的提示和技巧,最后签字已经成为真正的在过去的几年里。

荷迪:此外,我们认为验证应用程序的关键。应用程序使您能够为大众解决验证的问题,而不是一些专家。一个大障碍正式技术的引入已经断言。验证人,特别是设计师,不知道如何或不喜欢写断言。应用自动化问题,断言的创建针对一个特定的验证问题。

Kelf:我们可以考虑我们需要正式的第二代。第一代是笨拙的,有些学术技术,然后我们看到这种快速转向应用级方法。真正意图等公司的业务模式与时钟域交叉(CDC)解决方案,这是我所说的第二代。现在的问题是我们如何搬到第三代,在核心断言是必需的。

莎当然提高产能,增加,远远超出了计算机的速度。第二个变化是,人们已经学会了去哪里申请正式和使用它,它可以让一个真正的区别。最好的地方是范围狭窄和失效模式的完整理解。

Kelf:有地方模拟不能规模。

莎:是的,疾病预防控制中心是一个很好的例子。失效模式是一个融合的功能和时间,当这两个东西异步发生,模拟分崩离析。有越来越多的这样的地区。

Levia:除了能力,有很多的改进算法。没有一个正式的引擎。证明我们有超过一打不同的引擎,这使我们能够从小和深奥的迁移到大而复杂的问题。当我们看正式的问题可以解决,我们看到的范围几乎是无限的。这不仅仅是模拟不规模。有问题,模拟不能solve-dynamic能力验证,安全、连续的等价性检查,等等。正式的不仅是适当的,但必需的。正式从“高兴”的必须。已经改变的另一件事是,成功产生成功。正式的投资回报率高,影响了商业模式。 The high selling price associated with that attracts the attention of the decision makers. That ensures it is proliferated throughout an organization and success achieved. We predict that formal will eventually become the dominant verification approach with the assistance of simulation.

SE:早期的成功在疾控中心等领域,部分是因为你没有写断言,但到更高级别的验证,断言是必要的。我们如何克服这一障碍?

Singhal:断言语言只是SystemVerilog。你可以从一些非常基本的和研究生缓慢。您也可以编写参考模型、记分牌和完整的端到端证明,例如总线控制器,处理器、视频解码器,等等。一旦你已经学会了一些基本的东西,你得到了越来越多的成功,这使得你愿意投入更多。

莎:断言语言不仅仅是写检查,也是约束。有三个需要解决的事情。首先是规范缩小问题的范围,检查从理解隐含的失效模式。所以你不需要断言写检查,只约束。其次,限制允许我们控制范围的复杂性问题。第三,它使我们能够调试以通知的方式是可行的。

Levia断言:我们看到来自多个来源。也许最重要的一个今天是验证的IP。这些通常是跳棋,限制,和现在我们看到证据为常见的协议包。这些缓解需要重新创建它们。下一个来源是应用程序能够从更高层次规范生成自己的断言。连通性和X-propagation例子。然后我们可以断言我的模拟数据。最后,还有人写自己的断言。我们不再看到断言的限制。

莎:你必须确保你不会产生太多的低质量的断言,这可能是一个危险的矿业仿真数据。这种危险是可以避免通过了解前期的目标。

Kelf:当断言写作成为主流吗?Oz谈论的事情帮助,因为你可以看这些,从错误中学习。但是我们也相信,我们需要更好的工具来帮助写断言。

荷迪:我们讨论的是正式与模拟,如果是在竞争,这不是真的。他们是相辅相成的。人们要做的是实现基于验证计划验证关闭。所以测量的贡献是非常重要的。考虑unreachability报道。你可以模拟某一个点,然后分析点保持是否可及。这提供了一个巨大的投资回报,因为它的目标指示的地方测试很难写。注册验证映射是另一个例子,可以生成断言从其他规格,在这种情况下从IP-XACT。

Singhal:你必须注意整个金字塔。不是每个人都能写断言。有很多人使用应用程序不需要断言,但也会有一些人断言和专家需要它们,因为没有它们底层会步履蹒跚。在过去,如果没有这些人,断言只有最简单的写,因为这个他们没有看到ROI。

莎:在任何系统仿真是一个后备选择。你越了解一个问题,你可以申请一个正式的分析。设计步骤变得更加理解,有更多的地区适合正式的解决方案。

Kelf:但有正式和模拟之间的问题。如果我们看看今天的标准被创建,使用断言UVM是一场噩梦。UVM没有正式成立。最重要的是我们有uci,旨在汇集覆盖率信息。这也是simulation-centric。实现由工业和正式的标准组织有一个地方会是有用的。

Singhal:UVM有,我们必须适应一个模拟世界,它可以处理很多的事情,我们需要做的。

这个专家表系列的第2部分中,小组成员分析标准的问题,他们需要更新的领域。