正式的混乱

半导体工程坐下来讨论对与错方法应用形式验证技术Normando Montecillo,副技术总监博通公司;阿施施Darbari,首席工程师想象力的技术;罗杰·Sabbagh在华为首席工程师;PMC塞拉和斯图尔特•Hoad领导工程师/Microsemi。下面摘录的对话发生在解码正式,事件由Oski技术和由Synopsys对此。

SE:在模拟报道指标。我们都知道他们有多坏,但我们相信他们。和闭包在哪里形式验证吗?

Darbari:考虑线头。你没有testbench运行它。它找到bug和给你一个好的感觉的打线RTL的功能,但不是我们习惯于的报道模拟。如果您正在编写断言那么你有思考的需求,这就是我等同于完整性。完整性要求:我们覆盖的空间需求。有一个失踪的一部分在模拟和突变的一个方面,看看你可以检查失败。我们应该统一并想出一个数字。

Sabbagh:有一种感觉在正式的家伙,正式是完美的,它提供了一个证据。我们想要一个覆盖率度量是等价的。在现实中,我们没有在模拟和我们多年来一直生活在不完美的指标。我们已经足够好了。如果断言覆盖所有的功能设计基于结构覆盖点;如果他们粉丝断言;如果他们包含在抽象的证明地区——我们有有限的证据,让你知道如果结构覆盖点深度内的证明,我们有能力证明是可及的,如果事情仿真不能做。我们有大量的抛售我们所拥有的价值。签署了正式的能力是比和更严格的模拟。

Hoad:我不确定如果是更严格的,它是不同的,理解不同的是关键。

Sabbagh:除非你在模拟中使用突变的报道,这是非常昂贵的,你真的没有可观测性覆盖率度量。你可控制性指标,说我能够刺激一些设计的一部分,导致一些设计中的运用。产生正确的结果吗?我不知道。它可能产生一个糟糕的结果,没有传播检查器。甚至功能覆盖率不告诉你testbench检查任何结果。还很弱,我们依靠这些指标。

Montecillo今天:管理是适应模拟覆盖。正式的圣杯是达到这一点,我们的报道可以插进他们的报道,两国将合并,我们会每天想看到的100%的覆盖率。我们与模拟覆盖。我不确定如果我们能到达那里,因为这是一个非常困难的问题。正式我们严重依赖测试计划。跳棋的testplan告诉我们我们需要写,有什么约束,需要写,然后依靠连续深度分析到那里也看着遥不可及的,深度的证据。

Darbari:在短期内我们可以用模拟生成混合的指标。

Hoad:我们是到达那里。

Sabbagh:但是是正确的追逐?仅仅因为模拟一直这样做,我们为什么不能提高酒吧一点吗?是时候携起手来,真的搞定它。

SE:在过去一年中最大的突破是什么正式的使用和部署?

Hoad:可用性。越来越多的人可以使用一个正式的工具,迅速得到结果。如果他们的动机,他们可以更加努力与工具做不同的事情。现代正式的gui工具已经是最大的发展。

Montecillo:在过去的五年里,引擎也发达。五年前,我必须做为了得到更深层次的抽象。我今天使用的引擎,我不需要这样做。它对我和让我深入设计。报道正在取得进展,尽管它还没有我们想要的地方。

Sabbagh:方法是使或打破了游戏的一件事。IC3算法的发明是一个重大转折,它采用了几乎所有的供应商。由于这个原因,增加了可伸缩性。调试是一个任务,需要大量的时间和可用性帮助。不是所有的EDA工具相当那里。

SE:缺少什么?

Darbari:工程师需要做芯片和他们必须设计和验证。一路走来,调试故事迷路了,找到根源的能力一直是一个大问题。人们继续做他们所做的在过去。

Sabbagh:它是容易抛出一个反例,但是正式的一大挑战是如何调试一个遥不可及的点。你做什么工作?工具不提供支持。我们已经走了这么长一段路。我们有标准的断言语言,覆盖指标,我们有新引擎——我们已经走了这么长一段路。这使得它更实际使用正式的。

Montecillo:但它仍有很长的路要走。我们需要答案可伸缩性问题。我们还是看小块当我们想要实现的是一些更大。今天,我们必须把它或抽象或孤立的事情。

Sabbagh:它回到你想要正式。如果你想做端到端正式你想证明没有死锁的情况下,然后你必须聪明。我们需要继续进化。

Hoad我们需要让他们更容易预测。它是非常困难的,有经验,但是如果你不能有可预测的结果,那么你不能实际应用到一个新问题,因为你不能处理这个级别的不可预测性。

Sabbagh:正式将提高可预测性。

Hoad:只有一个定义良好的方法和定义的问题。

Darbari:它是一种使用正确的正确的任务

Sabbagh:基于仿真的方法,我们得到90%或95%的覆盖率,过去几个百分比的不可预测性。

SE:采用所面临的最大的挑战是什么?

Darbari:教育。它是关于确保人们理解它会给你带来什么,设置正确的期望,然后让人们去做,确保他们正确的事情传达给上级管理和处理的信息垂直从工程师到经理,让他们看到它以同样的方式。它是一项艰难的工作。

Sabbagh:有不同程度的接受。我中心团队的一部分,部署正式在我们的内部客户和不同的设计组织有不同程度的阻力或验收。这取决于你正和谁。一些组织也采取正式的自己,可以帮助。别人想要我们这样做,就像推绳子。

Hoad:是的,有惯性,取决于人们所遇到的问题,与正式的过去。

Montecillo:为了克服惯性,有资源问题和人才问题。教育是绝对。接下来的问题是:我们如何让人才团队,这样他们可以部署正式?我找到的最大的阻力是他们找不到必要的人才。我们应该开始将一些动态验证人或得到新的人吗?如果我们做得到额外的资源,你在哪里找到这些家伙吗?去年我想雇人的时候,我发出了一个请求,所有的简历我已经回来的UVM体验。没有一个正式的经验。我们发现的是孩子,只是大学,愿意做这项工作。其中一些没有背景的模拟是伟大的。他们没有被损坏。

Hoad:对。如果你认为事情的指导测试用例,很难考虑如何构建正式测试。

Montecillo:当我们把人们从模拟,他们做的第一件事——他们写一个导演在正式测试,我们必须扭转思维,需要一些时间。

为验证团队考虑正式SE:任何建议吗?

Sabbagh:去吧。

Montecillo:攻击低挂水果——诸如连接错误打猎,断言/属性自动生成。他们将展示一些立即的成功。不解决一些比你可以处理。一旦你失败了,你又要在这有限的机会。

Hoad:计划它,这样你得到好价值。

Darbari:与一个已知的东西后增值。

有关的故事
正式的混乱第1部分
应用形式验证的最佳方式是什么?一些行业的顶级用户有不同的意见。
开放标准验证吗?
压力构建提供常用方法使用验证结果分析和测试目的。
一个正式的转换
当你把正式的领导人来自世界各地在同一个房间里,给他们一个小时讨论部署?