深或广泛的正式呢?

是否适用形式验证技术半导体设计广泛或深是一个很难的问题。它取决于什么是最好的方式来获得最大的投资回报率。

你想确定很难找到错误,并得到一定程度的信心一块呢?努力应该放在哪里?是通过深度,这意味着一个团队的专家或专家必须建立正式可以使用先进的技术,和做事情,不是每个人都可以做的,但他们可以找到漏洞,其他工具或技术找不到吗?或者是正确的方法广泛,不同的应用程序使用的平均验证工程师或设计师可以从中获得真正的价值时,发现错误?

事实是,深度和广泛领域的投资回报率高,据。“问题可以归结为多少时间和投资一个愿,”肖恩Safarpour说,CAE主任正式的解决方案Synopsys对此。“如果时间是稀缺的,那么要和一些正式的广泛应用是一个快速的解决方案,提供了大量的价值。应用如连通性检查或正式注册验证可以部署在几天内,但可以节省几周的仿真工作,以及很快发现bug。他们所做的这一切不需要火车任何人“高级”正式的技术。”

大约有十几个这样的应用程序验证经理可以利用很少的投资。另一方面,如果一个人有能力来训练一个工程师在正式验证基础或雇佣一些正式的验证经验,然后他们可以部署在深度域和形式验证捕获仿真或其他高价值的错误找不到验证技术。

”在这种情况下,正式的所有者将编写特定属性和在一些已知的漏洞,会发现质量缺陷或给管理高水平的信心,“Safarpour说。

皮特•荷迪产品管理总监节奏表示同意。“深或广泛并不是互斥的选择。主要客户都在两个阵营,至少某种程度上。正式的应用程序自动生成属性使形式验证可用一般验证工程师和设计师不熟悉上海广电(SystemVerilog断言)。例如,连接检查在正式是接近显而易见的事情。通常更容易、更方便比乏味的基于仿真的方法,”他说。

所使用的技术也与模拟给正式证明努力改善一个模拟testbench报道DUT的某些部分被测试(设计)不会给所需的覆盖改善。通常可以节省许多周每DUT的浪费精力,不需要编写任何财产,荷迪说。“这是不仅仅是验证工程师。能够自动生成属性补充结构线头有价值的功能检查(节奏称之为Superlint)被证明是非常受欢迎的设计师。这使得它可以检查算法和循环溢出,FSM活动锁和死锁,以及一系列的其他检查之前用最小的努力把设计了完整的功能验证。”

据说,“应用程序”的概念也许7到8年前开始,毫无疑问,促成了“民主化”的正式验证。“然而,尽管随时可用,这些应用程序服务特定的验证任务,因此有限范围几乎可以确定的是,“荷迪说。“他们不开始挑战仿真的主要的主力的位置,功能验证,但它们确实很好地补充。以来发生了什么是,所有领先的半导体公司的投资也在迅速增长正式的深处,我的意思是使用正式的验证通过写一些自己的属性。”

很难夸大的作用应用在广泛的扩张形式验证的使用。

“通过解决具体问题,应用程序很容易理解的价值,”塞吉奥Marchese说,技术营销经理OneSpin解决方案。“许多应用程序不需要的知识断言或正式的算法。在他们最好的,使用正式的应用程序一样容易运行传统的“棉絮”检查而发现更严重的设计缺陷。应用程序也作为第一步到正式的验证。用户连接检查可能会发现几个约束条件必须得到准确的结果,继续尝试写作和证明一些断言。”

此外,另外使用断言来说是无价的,。“事实上,另外两个应用程序和高级assertions-from简单,端到端验证流的旅行社提供巨大的价值,无论是从效率和发现更多的错误,“Marchese说。“此外,都可以做一些模拟或仿真不能做,这是证明没有bug的功能验证。应用程序只需要很少的投资,是一种简单的选择对于大多数项目。正式的签字需要专业知识,许多公司还没有内部。投资外包或建筑专业知识是否值得,取决于项目/公司。像汽车和航空安全性至关重要的应用程序,或应用硬件安全是一个主要问题,使用专用的正式程序和实现正式签字,至少具体的关键功能,可能是一个不可避免的选择。”

荷迪指出,许多动力驱动的快速采用深正式:

• 巨大的改进形式验证工具的可伸缩性。设计与数千万甚至数亿盖茨现在可以处理。尽管盖茨并不是一个非常好的测量形式分析的复杂性,因为它的状态空间,已经完成了大量的工作增加产能和开发更好的方法和指导设计类型是比其他人更适合正式的。结果是深层形式验证可以应用于更多的典型芯片设计不仅仅是几年前。
• 技术超出了纯粹的能力。抽象属性分解,生成辅助属性,拥有多家发动机,和其他改善了正式的性能和收敛性。这是自动的工具,减少深知识的必要性。
• 大多数现代正式专家不再专注于实现“完整的证明。”分析工具,帮助工程团队理解是否“有界证明”(即。,证明持有好一定数量的周期)是一个足够好的结果。
• Bug狩猎方法已经出现。这允许用户很容易找到深刻的反例(CEX)痕迹。这些方法是由端到端性能,但发现困难,高价值的错误的全部期望推动房地产永远不会证明。这些方法补充仿真和经常可以用来发现bug,深深的角落几乎不可能编写约束随机测试。某些方法来执行这个bug狩猎经常出现重要bug甚至在成熟的设计,以及导致覆盖指标,增加了信心,没有bug。

方法问题
应用形式验证技术的一个重要的考虑是能够使其设计过程中不可分割的一部分。

据乔Hupcey,验证产品技术专家导师,西门子业务,在这里,正式的应用程序和他所谓的“直接财产检查”彼此独立的客户提供伟大的价值。“不过,有一件事我们看到一直在许多客户是formal-based应用帮助设计和验证工程师“跨越鸿沟”,直接开始使用正式的验证。通常,客户得到他们的脚湿formal-based连通性检查应用程序因为效率和易用性的流动无疑是数量级比基于仿真的方法。”

然后,在下一个项目工程团队尝试更多的正式应用相应的验证需求。

“即使用户已经准备好期待好的结果,“新”应用程序的有效性经常超过客户已经很高的期望,”Hupcey说。“由于应用正式的成功应用,这些团队不可避免地开始看应用形式分析。他们开始“bug狩猎”在特定的设计元素,并继续掌握技术关键功能的充分证明。关键是这个工作收入与其他设计上运行应用程序块,所以总的结果是客户继续使用应用程序和正式的属性一起检查。”

基本上,一旦正式介绍了相当大的权力和利益的一系列正式的程序,没有回头,正式成为一个永久的一部分用户的验证工具。

最后,那些说属性很难编写或正式的工具很难使用,抑扬顿挫的荷迪指出,他们分为两个阵营。第一个涉及工程师不再直接验证和不知道如何惊人复杂的创建UVM testbenches SystemVerilog充分验证当今复杂的芯片。

“从概念上讲,他们得到的模拟比正式的,但他们留下了在现实的模拟变得是多么的复杂,以及多少可以用正式的有效实现。另一阵营是彻底的UVM / constrained-random专家。他们知道他们所知道的,他们坚持它,”他说。