一个正式的转换

一个非常重要的改变正在进行功能验证。在过去,这是一个深奥的技术,是一项难以部署。是降级的难题在验证周期的后期,并很难证明ROI,除非技术实际上确实发现了一些问题。但是所有的这些已经改变了。形式验证公司开始使用这项技术的解决方案。

半导体公司开始部署这些解决方案来解决他们的设计选择验证问题。这些解决方案解决狭窄的、定义良好的问题和他们的方式不需要了解所使用的算法。这将正式从富人的工具变成了一个不可或缺的工具。

这是第一阶段的转换。现在第二阶段正在进行中。形式验证不再仅仅是一个后端工具,但在许多情况下被视为第一验证工具部署——很久以前模拟testbenches准备好了。半导体工程被邀请参加什么可能是最神奇的正式的领导人曾经聚集在一个房间,讨论正式的部署。15专家来自世界的各个角落,从街对面。事件是由Oski技术,一个正式的验证服务公司。

找到合适的工作的工具

事件从一个主题开始由Dan Lenoski赤脚工程网络的联合创始人兼副总裁。他谈到他的公司面临的具体挑战的高性能网络,特别是它所面临的核查问题与新软件定义开关。

“很多查找问题是更复杂的比大多数人猜,”解释Lenoski当他经过系统的各种元素。“它包括诸如最长前缀匹配和ACL查找,这常常需要TCAM查找和可能包含通配符或“不关心”,可能包括的范围。如果它是一个固定的管道,你需要一个架构参考模型,你可以做很多基于随机测试和对某些碎片。正式的检查是可能的。”

Lenoski解释内存体系结构如何影响系统的性能,甚至导致包下降。他说,验证是非常困难的。“调试也是困难的。你会突然看到垃圾出来,或因为内存泄漏的你开始有问题两秒。需要成千上万的周期之间的有趣的事件。”

正式不能直接应用到这类问题不聪明。“你不需要考虑64字节;1个字节。你不需要所有的队列。我们已经成功使用正式的帮助验证这些类型的问题。”

这些都是过去的问题。“我们现在看到使系统更加灵活。P4你可以把协议描述语言,并使用一个编译器,地图的不同阶段的新架构。之前,你必须re-spin ASIC修改管道,但现在我们可以定义的一个软件,达到相同的性能。然而,它确实增加验证挑战。”

Lenoski和他的团队仍在制定最佳方式正式应用于问题,包括使用P4上的正式描述或等价性检查它和编译器的输出之间的关系。“我们需要优秀的技术来完成工作,并且需要约束的随机的,经过验证的贵宾,模拟和正式的方法。”

主题是一个圆桌会议后的谈话。下面是讨论的概括。大多数的与会者要求他们不能直接引用,所以所有评论转述,匿名的。与会者提供的完整列表的最后。

坐(左,右):戴夫•帕里Youngsik Kim Ram Narayan Ashish Darbari,赛义德·哈姆
站(左,右):阿里·哈比比杰西·宾厄姆(photobomber从英特尔得主Oski棋盘挑战),理查德Ho Normando Montecillo,斯图尔特·Hoad罗杰·Sabbagh Vikram Khosa却Vigyan Singhal, Viresh派鲁锡,埃里克·塞利格曼,Swapnajit Mitra丹Lenoski

定义正式的ROI

戴夫•帕里Oski首席运营官,让他们开始问他们如何在各自的公司提出正式的ROI。

一种方法是定义一个保险的方法。“为了证明正式好保险我们必须结合功能和正式的功能验证快速发现问题和错误等问题,编译错误。然后正式进入和数字根深蒂固的问题。这是非常成功的。我不确定如果这增加ROI,但它使正式更有价值,因为它提供了一个很好的方法来部署。”

其他人都在尝试不同的部署方法。“我们曾经让功能验证几个月做的事情,然后正式开始使用。发现的错误数的正式的总是少但质量高。现在我们正在尝试修改方法部署正式在早期。与正式的您可以编写一个封面财产,使用一个工具可以画出痕迹,按下按钮。我们也看到了设计师想要证明的断言。这提供了动机写跳棋在早期,这有助于长期。”

的几个成员确认正式使用更多的在设计的早期阶段,但他们必须对抗认为正式被用于错误,越容易模拟早晚都能找到。“这并不是简单的bug。如果你部署正式在早期可能会打击一些角落。目标是把bug被发现在这个过程中,早。”

指出两种不同的东西被讨论。“有动机post-silicon bug或类型的设计,非常formal-leaning,你想把正式的。还有另一个线程的早期形式,因为它比其他方法更有效。我们必须分开这两个使用模型,因为他们有不同的投资回报。”

另一个人提醒如何定义ROI。“当使用正式的,工程师往往设置他们的环境,但他们没有任何错误报告文件,因为他们只是修复bug,因为他们发现他们。这意味着管理假设他们没有发现任何与正式的bug。”这其中的一个反应系统中必须有反馈,以确保管理知道所提供的价值。

这导致了一场激烈的争论的价值计算错误的测量善良。“这不是一件坏事,如果我找不到错误!最好的方法是发现尽可能多的错误可以在一些项目,他们可以找到他们在模拟更快。这不是一场竞赛。”

有一个普遍的共识,食物必须停止战斗。的一个成员在其公司的讲述一个故事。“在一个设计,正式发现几个重要bug tapeout之前和管理团队收到了很多的关注和赞扬。然而,在另一个团队,正式的没有发现错误但却获得正确性的证明。他们没有获得表扬或关注。“他人同意验证团队不应该奖励基于错误的发现,尤其是如果你得到一个很好的设计师创造了一些bug。

正式的应该应用在哪里

得到正式部署的另一种方法是看问题很难模拟,但容易正式。一个成员说“我们做的第一件事扩大正式考虑高层多路复用技术。我们有一个芯片的核心,然后使用外部I / o多路复用技术。结构简单,我们用来做仿真,但大约需要两个星期。问题是,你要做tapeout前的最后的事情。与正式的你可以做到6个小时。如果你管理,你获得必要的资源。”

有几个想法就正式的应用场合。“没有理由做同样的模拟可以找到的东西。这是一个浪费时间。一些街区非常在模拟或最适合模拟验证。遗留的设计,一切都已经到位,这是最好的留给一个仿真环境。是没有意义的试图用正式代替它。”

但并不是所有的同意。“有情况模拟只能找到一百万年之后。它不可能是什么。如果有一个巨大的重叠在你寻找的类型的bug,然后我同意将更具挑战性的证明。在新的设计中,任何人都可以使用任何技术发现bug。但是你可以展示设计师的一些错误,你发现通过正式在模拟几乎找不到,因为他们是嵌套的FSM的深处。时间是一个重要方面,因为一切都是相关的。”

解决这个问题的一个方法是去处理它验证计划阶段。现在,它只是一个问题的验证任务被分配到模拟、仿真和正式的,他们每个人的工作分配。这纯粹是基于能力的工具。“有很多遗产模拟testbenches和那些已经开发的测试用例。我们不会扔掉它们,停止做模拟。攻击的并发性SoC水平,我们使用模拟。没有类似的解决方案。以FPGA可以实现5兆赫左右,所以你可以把一些软件。如果你坚持模拟,这是不可能的。与正式的是相似的。领域被很好地定义,它可以为正式的琐碎但很复杂的仿真。每个人都有一个利基。”

但有些时候遗留的设计变化的方式会导致重新评估。这可能是错误发现,改变频率或技术变化。添加到最初的开发人员设计的混合或testbench可能不再是可用的和一个简单的修改遗留模拟环境的可能不再是最好的方法。

谁应该正式运行?

提出的另一个问题是建设团队和谁应该运用正式的。“我没有成功让设计师使用正式的早期阶段。设计师是谁试图不做一个很好的工作。成功的人是一个非常小的比例。我们发现更好的是让一个高素质的人做正式的验证。他们可以做超过三个设计师。”

再次讨论分为那些正在寻找深层问题与那些试图使用它在设计过程的早期。“设计师可以很深入设计,但有时会更抽象可以导致更多有趣的测试用例。你需要两者的结合。”

尽管协议设计师保存基本信息,使验证简单,这只是一部分所需要完成的任务。“这是一个挑战来写断言。它需要一定的心态。当我看着断言我们今天写,很多人模仿RTL。真的很难改变心态,说,不是我们想要的。”

那么,谁应该写断言?“所有的成功与实现形式验证没有一个断言是由设计师。所有的断言和属性是由验证小组完成的。今天的设计师是不堪重负。设计师设计。验证人负责写属性来验证设计,而婚姻是令人满意的,我们有100%的支持每一个设计师和验证团队已正式应用。”

没有达到结论验证团队中的人的灵活性。一些人担心testbenches建设往往是非常低效的,但是这不是一个问题的模拟。然而,当处理正式技术,效率是最重要的,如果结果是可以预料到的。再需要一个不同的心态,不同的品质部署正式。与其他部分的讨论,这取决于不同深度缺陷目标或者是使用正式的应用程序是针对特定问题。

很明显,正式被用于越来越多的全球最大的半导体公司。我们过去阶段正式必须是合理的。更一个疑问的地方的好处是最伟大的,和这个话题仍有大量的讨论。

参与者包括:阿里·哈比比高通;理查德•Ho谷歌;Swapnajit Mitra Avago;阿施施Darbari,想象力的技术;Vikram Khosa却手臂;Ram Narayan,甲骨文;埃里克•塞利格曼英特尔;罗杰·Sabbagh华为;Youngsik金,三星;斯图尔特·HoadMicrosemi公司;Normando Montecillo,博通公司;赛义德·哈姆,Nvidia;Viresh派鲁锡,IBM和丹Lenoski赤脚网络。

有关的故事
验证面临独特的拐点
得到正式的关于调试
调试:自动化的最后堡垒