正式的路线图

形式验证已经在过去的五年里取得了长足的进步,因为它专注于狭窄的任务验证流中。半导体工程坐下来讨论的进展和未来的正式技术,总裁兼首席执行官OneSpin解决方案;哈里·福斯特首席科学家验证导师图形;皮特•荷迪产品管理总监节奏;首席架构师Manish Pandey新技术Synopsys对此;的首席执行官Agnisys;,总裁兼首席执行官Oski技术。以下是摘录的谈话。

SE:正式不再被认为是一个利基技术。如何有进步在正式被半导体公司意识到,和它又是怎样影响验证方法?

Singhal:我不认为形式验证可以被认为是一个利基技术,没有相当长一段时间了。重要的是理解你想做什么正式的验证。你是想解决当地问题,包括等价性检查,时钟域交叉(CDC),应用程序,断言块级别验证?取决于你想做什么,这可能是利基技术。有很多问题哪里有well-adopted技术。对很多人来说,现在正式批准过程的一部分。然而,存在一些问题,如系统验证,仍然使用模拟。

荷迪:正式穿过峡谷,超出利基在这个阶段。17日我们正式的产品在使用的前20名半导体公司。你不去用它还在一个利基技术。它已经成为是一个“必须”验证。剩下的唯一问题是总数的多少验证任务可以应付。你仍然需要不同的验证引擎的不同部分的问题。如果你不使用正式在至少知识产权或子系统验证,那么你在后面。

Pandey:正式的不再是一个利基。每一个认真芯片设计房子是使用它。等价性检查是第一个正式的技术,但是我们不叫它正式的了,因为它是成功的。如果你看看正式属性验证,使用这样的方法越来越标准化,有正式的IPs。正式不是很欣赏的一个区域是,即使你看问题,如连接,检查和属性低功率,有技术与正式罩下面用于帮助改善结果的质量。偷偷在缓慢而稳定。按钮技术倾向于应用和人们非常成功。在许多情况下,他们甚至不知道他们正在使用正式的。

福斯特:一个不同寻常的事情我们看到(忽略等价性检查和自动程序关注某些问题)是在2014年和2016年之间有巨大的增长的正式产权检查。在2014年之前相对平坦。增长约26%。大约33%的所有设计都使用正式的属性检查。如果你去更先进的设计,那些超过8000万岁的盖茨,你在45%或接近50%渗透到这些大型的设计。如果你分区更远、更大的设计,我们看到更多的采用。到底是什么原因导致了这些在某些领域是安全的。45%的设计都属于安全在某种程度上,如必须符合ISO 26262, - 254或其他人。更重要的是,67%的设计是实现某种形式的安全特性。正式这些类是一个伟大的技术设计。

问题我们使用正式的。我不知道这是一个利基市场,但它是生长在意义。我们看到它被更多的用于连接和注册验证。我们希望看到更多的发生。验证仍在使用,你不能离开UVM。你不能仅仅按下一个按钮,和正式的一切做了。

Brinkmann:这取决于顾客。在一些地区,它已经变得根深蒂固。我们有一些汽车客户,这是他们IP开发过程的一个组成部分,完全是依靠他们的IP块。他们做了完整的证据,然后他们确信他们正在开发的上下文中工作环境和不同的设置。在其他地方,它更多的是一种技术来发现错误。

SE:我们通常不包括等价性检查当我们谈到正式,让我们不包括疾病预防控制中心或X验证或者一些人。似乎是给定一个名字时就解决问题,不再是正式的桶。

福斯特:是的,这部分是一个营销的事情。当你说正式的,人的眼睛闪耀着,所以我们想隐藏的正式名称。但是经常有一个正式的引擎。

荷迪逻辑等价性检查:这是真的,但连续的等价性检查更多的是一种基于属性的技术。这可能是真正的疾病预防控制中心。所以对于X-prop少。有一个正式的截然不同的好处和模拟。在正式,如果你X-prop得当,你没有悲观或乐观情绪问题。你可以模型正确,检查它彻底RTL和唯一的问题是可伸缩性。我可以重置验证一个整体吗SoC吗?也许这就是延伸一点,但正式和仿真的结合可以解决这个问题。从根本上讲,X-prop和正式没有模拟中存在的问题。

SE:新兴的正式技术应用几乎准备好有一个名字?

Singhal:系统级验证。这些天我们在做建筑形式验证。我们正在考虑安全之类的缓存一致性。很多人感兴趣的证明没有上下文切换时系统级死锁或系统如何执行。这些都是正式的和大难题一直远离。通常不能在这样一个大系统,不仅正式工具的今天,明天的人。所以你必须回去和分解问题和应用架构验证的方式可以解决piece-meal时尚,然后缝合一起证明到系统级需求。

福斯特:我看到了一个成熟的行业,它不再是人们购买一个工具。它被系统化的方式与资源到位致力于这样做,到位测试计划整个过程方面,过去被忽视了。这就是为什么我们看到应用程序之外的迅速采用纯正式财产检查。

Pandey:有公司现在要求每一个块都有正式验证。他们有专门的工程师正式。没有正式签字,确认不被认为是完整的。很多方法被开发来帮助定义如何事情应该在系统级验证。当你想到诸如连接,这听起来像一个简单的问题,但如果你把一个设计有几亿盖茨不是一个微不足道的问题。它既是正式结合设计代表和高效的启发式。使用正式的我们可以修剪的事情。

Brinkmann:在安全方面,仍有很多工作要做正式的。故障传播分析是另一个领域,你会听到很多关于这也是能力的识别un-propagatable故障是否可以证明,这样你就可以得到你的诊断范围所需的水平。在function-safety验证你必须满足一些报道标准,和正式的唯一方法是缺乏一些东西,所以得到很多好处。

荷迪:就像我们会从一个极端到另一个。当你把连接,这是一个任务,你需要使用正式的,因为它没有意义去做模拟。然而,您可以使用正式的事情很难做仿真,因为能够正确分类的缺点,根据ISO 26262,你绝对需要能够证明一个问题不能输出或传播,此外,它总是检查,总是被检查。这是极其困难的。最好的你做模拟是指一个测试用例,这表明它是传播到一个输出,或者告诉我当我还没有测试用例或检查器可以选择这个。正式的绝对更能回答这些问题。

有关的故事
执行官的洞察力:Raik Brinkmann
OneSpin首席执行官看着形式验证为什么突然必备的技术。
差距在验证流程
专家在餐桌上,第3部分:小组成员讨论软件验证,SystemC和未来技术将有助于验证跟上。
开放标准验证吗?
压力构建提供常用方法使用验证结果分析和测试目的。