正式的路线图

正式核查在过去五年中取得了很大进展，因为它集中于核查流程中的狭隘任务。半导体工程坐下来讨论的进展，以及正式技术的未来，与，总裁兼首席执行官OneSpin解决方案；哈里·福斯特，首席验证科学家导师图形；Pete Hardee，产品管理总监节奏；Manish Pandey，新技术的首席架构师Synopsys对此；， CEOAgnisys；的总裁兼首席执行官Oski技术．以下是那次谈话的节选。第一部分可以找到在这里．第二部分是在这里．

SE:当Mentor开始验证调查时，SystemVerilog而且UVM尽管80%的行业还在做定向测试，但我们还是做得很好。我们确实倾向于关注最高级的用户。采用的范围有多广形式验证？还是只有顶级用户?

福斯特:我将调查数据按照设计尺寸进行划分，小于5M门，5M - 80M门，大于80M门。这并不是一个完美的1/3,1/3,1/3的分割，但有趣的是，设计越小，就越有可能出现衍生。我过滤掉了模拟问题。然后我研究了各种技术的采用，例如代码覆盖率设计规模越大，这些技术的应用就越多。有了真正先进的设计，我们的使用率超过了50%。让我来谈谈一些不太正式的公司。他们仍然可能使用一些正式的应用程序。这些公司倾向于大量购买知识产权做积分。但是他们仍然在使用正式的连接方式。开发内部IP的公司往往是采用正式形式的公司。

Pandey:今天开始的每一个新设计，不仅仅是技术的重新映射，都计划使用正式的。他们可能会在区块级别进行属性验证，并使用其他正式的应用程序。进行属性验证仍然存在一定程度的痛苦。但现在的痛苦阈值更高了，效率更好了，价值也更高了。人们看到了更多的价值，也愿意更加耐心和宽容。

Singhal当前，如果人们不使用正式用语，就会遭到殴打，这是过去的逆转。

福斯特:看看FPGA空间。只有大约20%的fpga在交付给客户时能够正常工作。在某些市场，我们不能在不打开整个盒子的情况下重新验证，比如汽车和航空航天，所以成本是巨大的。我们开始看到FPGA设计采用形式化，这是我从未想过会发生的事情。目前，我们在FPGA设计中采用形式化属性检查的比例接近20%。

Brinkmann:我们也看到很多人采用了等价性检查。我们做顺序检查合成进入FPGA，这就是他们购买它的原因。它不便宜，以前的人会说它是一个FPGA，只是重新运行它，但这不再工作。如果没有巨大的成本，就无法打开它并更改FPGA。

福斯特:什么时候问题比解决方案更令人痛苦?我们已经越过了这一点，解决方案也变得不那么痛苦了。

SE:几年前，在形式化算法上有了一个突破，使每个人的性能都有了显著的提升。模拟这表明当你不能持续提供收益时会发生什么。正式如何避免这些问题呢?

福斯特:狭窄的应用程序意味着更多的问题变得易于处理。

Singhal:如果你看看整个计算机科学领域，包括图形学、计算机视觉、编程语言和数据库，最高奖项是图灵奖。这相当于我们的诺贝尔奖。在过去的20年里，有三位获奖者都在正式验证领域工作。事实上，计算机科学领域超过15%的顶尖人才都在从事正式工作，而只有不到0.1%的程序员集中在正式工作上，这表明该领域非常困难，但尽管如此，突破是巨大的，这已经转化为最终用户的很多东西。这些突破是如此巨大，它们使我们能够解决更困难的问题。进化的速度是惊人的。

Pandey:从发动机的角度来看，我们正在不断地推动边界，以提供巨大的改进。但是你想要在设计中阅读，你想要与仿真一致，我们就必须考虑各个方面的验证。我们必须考虑覆盖范围。我们需要有一个统一的观点。这些都是收养的重要问题。你不能让正式的验证成为孤岛。这需要大量艰苦的工程工作，以确保我们可以消化相同的设计或设计数据库，我们可以调试在框架内。因此，从引擎和接口来看，它们必须是连续的，这样才能使正式成功。

Brinkmann我们在很大程度上依赖于学术界提供的突破。我们必须做的一件事是为学术界提供资源，我们必须支持他们的努力，让在那里工作变得有吸引力。我们看到很多计算机科学教授说它不再那么有趣了，因为EDA不有趣，在那里赚不到多少钱。但如果我们不对基础研究进行投资，我们就必须继续让它吸引聪明的人。这是继续前进的方法。

Pandey:我读过关于人工智能(AI)的文章，事实上，正式的概念源于人工智能。所以我们必须在学术界培养这样的人才。

福斯特没有一个单一的解决方案可以解决所有问题。就形式和与模拟的关系而言，这是一个连续体。还有一些事情我需要验证，比如在正式场合表现得不那么有效。在这些级别上使用数据挖掘技术可能要好得多。我讨厌只关注工具。我们必须考虑整个问题。我们如何决定用什么来解决什么问题?重要的是我是否有合适的候选人，合适的资源。

荷迪在达到进一步的限制之前，有很多空间留给正式。我们在产能方面取得了很多突破。共同的编译和细化是至关重要的，这可能就是能力限制所在。就引擎而言，与仿真相比，并行化是相当容易的。我们有引擎编排，可以并行地证明属性，从而有效地利用计算场。我们有各种指标表明，就利用率而言，正式模拟的效益是2倍。那里也有足够的发展空间。

SE:近来神经网络引起了很多人的兴趣。这些为核查创造了挑战和机会。你如何验证机器已经学会了什么?神经技术会给正式场合带来机会吗?

Singhal:这是一个巨大的领域，但商业工具的服务严重不足。挑战在于，随着正式的应用越来越多，你将不得不随着设计的变化而逐步运行回归。如果你能学到昨天、上周、两周前同样的设计是怎么做的——它们与今天的设计95%相同——你就可以应用过去的结果。如果您正在运行完全相同的设计，即使没有任何变化，人们仍然会在一夜之间运行回归。有那么多的时间被浪费了，有那么多的东西可以学习。IT部门关心的是计算成本和农场的增长失控。如果我能通过学习更好地管理它，无论是模拟设计的形式，并尝试预测需要做什么。

福斯特:这是一个大数据分析问题，也是EDA中更有趣的领域之一。

Brinkmann:我们如何从机器学习中受益，以及什么形式可以有助于神经网络的验证，这是两个非常困难的问题。这是今天的一个研究领域。你要问的第一个问题是，“关于它你想知道什么?”正确是什么意思?”汽车行业对传感器融合和芯片计算机视觉非常感兴趣，他们需要这些技术来实现工作，所以问题就来了，“如何验证它?”

问题:这不是软件问题而不是硬件问题吗?

Brinkmann你必须把计算带到传感器上，这不是在软件上完成的，而是在硬件上完成的，因为功率的原因。人们将神经网络植入芯片，并在硅中实现。这就是你如何获得所需的低功率和密度。它们产生了大量的数据，由于延迟和电源原因，你无法足够快地从芯片上获取数据，也无法在数据中心进行分析。这一切都发生在传感器中，这就是它变成硅的地方。这意味着这是一个EDA和硬件验证问题。

荷迪:我们看到形式已经被应用到控制逻辑、协议、数据传输而不是数据转换的传统领域。我们正在推后边界，我们看到形式在数据转换中也很有用。因此，随着性能的提高，我们能够承担更多的问题。

Brinkmann:在这些场合，正式是很好的选择。如果你使用定点算法分析一个管道过滤器函数，然后想要知道导致溢出的条件，这是非常困难的，但你可以相当快地运行形式，得出一个输入序列，使你能够探索这些角落的情况，这是一个你可以非常有效地使用形式结合模拟来导航的领域。

有关的故事
正式的路线图
第1部分:小组成员将讨论在过去五年中formal所取得的进展，以及我们可以期待在哪里看到新功能的出现。
正式的路线图
第2部分:对正式规范的需求，覆盖范围和模拟的正式验证的进展。
填补机器学习中的漏洞
第2部分:确保机器按预期运行的短期和长期解决方案。