正式的新面孔

半导体工程坐下来讨论最近的增长与劳伦斯Loh采用正式的技术和工具,产品工程组主任节奏高级研发经理Praveen女子,验证小组Synopsys对此哈里•福斯特首席科学家导师图形,Normando Montecillo副技术总监博通公司和Pranav莎,首席技术官真正的意图。下面摘录,谈话。

SE:形式验证在过去几年已遇到越来越多的采用。这是高峰还是有更多的来吗?

莎:研究正式发生了几十年。的坐在解算器在50年代首次提出。在过去十年的设计和实现过程复杂soc已经稳定,成为更好的理解。结果,在这个过程中,地方的错误是由结晶。这给了正式的技术关注的东西,结果是失败的地方随处可见和灾难性的地方适合正式的技术。范围较窄,失效模式被很好地定义,这使得正式成为固定。一个很好的例子是时钟域交叉(CDC)。一个SoC的接口和一个典型的接口是异步的,这创造了一层复杂性。但复杂性并不与SoC的规模增长。

福斯特:正式的应用程序的第二个增长最快的部分EDA。模拟是最快的。正式的采用增加了27%。有两个主要类型的正式。第一个是正式财产检查,用户的负担坐下来写断言,另一种是目光狭隘的问题,我们可以把技术上的问题,减轻了用户的负担。第二个例子是,发生了变化,导致了增长。纯正式财产检查只看到经济增长在1%到2%范围内。

Loh我想添加一个第三项的正式类型列表。在过去的客户说他们有很多验证之前他们甚至要正式,但现在不是了。有古典产权验证,虽然增长放缓是一个领域,人们可以记录值。可以计算投资回报率(ROI)。我看到了两种类型的应用程序。一个类别的应用程序,你可以取代今天可以做的事情,但很多正式的版本更快更好。人们现在已经批准这些类型的应用程序的标准。一个例子是连接和控制状态寄存器,也许吧X验证。第三类是困难的问题。疾病预防控制中心可以检查常规结构检查不能发现的东西。另一个例子是低功率。这很难。

Montecillo:一件事对我们来说至关重要覆盖率度量。覆盖的数据库是非常重要的。能够衡量我们能够结合正式报道成一个单一的指标是非常重要的。在过去,总有一个论点,这是很难看到正式的价值,但现在它变得容易得多。模型检测,而只有百分之几的人这样做,这仍然是一个关键领域,我们要成长。模型检测的ROI是大。工具一直在发展,使它更容易为那些只有一点正式的背景使用。从五年前这是一个巨大的进步。调试工具能力也在迅速增长。我们也看到工具融合仿真和正式的。 An example is the waveform viewer that looks similar to those we have used in the past.

女子:我们需要看看横向和垂直。水平,我的意思是,正式要求专家和试图完成一个目标。如何融入到整个验证流?信心是什么?我们如何衡量,这是打在总体验证周期的一部分吗?考虑低功率或疾病预防控制中心。这些检查用来做仿真,,他们已经被正式取代。它允许您关闭并通过验证周期比其他方法更快。发现这些覆盖率度量和把它回到原来的指标是非常重要的。当我们看正式需要大量的专业知识,这是一个利基领域。 Staffing a project and managing it within an aggressive set of timelines is not easy. Also, how do you sign off on formal? People are looking at mechanisms that consistently achieve a goal in a specified timeframe and allow you to sign off on it.

莎我想挑战,正式成为一个利基。过去,端到端正式仍然是困难的。但我们不再看到正式作为一种工具。这是一个额外的武器军械库中解决问题。我们解决这些问题。

福斯特:安全。一切都结束了,但是明确的重点。

莎:我们使用正式的解决这一问题,模拟或深层语义分析。他们都可以用在正确的地方。我们不再认为自己作为一个正式的公司,但是作为一个验证解决方案的公司。而言,模拟和正式的,在过去的日子里,医学是在起步阶段,如果有任何疾病,治疗是放血。仿真是这样的。”我的芯片有问题。我需要模拟找出发生了什么。“我们了解更多关于为什么事情出错,技术已经更多关于如何缩小问题并找到问题的根源。

福斯特:我同意,但我要澄清。你说需要一个高水平的专业知识,和我从来没有发现一个成功的组织,没有增长所需的专业知识当试图使用端到端正式。它可以被收购,但这并不是你可以手的人。这不是说不同的人,去做约束随机的。你必须学习一些必要的技巧。另一件事是我们的行业,我们谈论正式使用这些工具,然而,许多人甚至不知道正式出现在那里。我们使用的是正式的技术来解决特定的问题,他们甚至没有意识到。

SE:该行业已经停止东西称之为正式当它开始得到采用。

福斯特:我们这个行业本身伤害早在90年代,当我们介绍了很多正式的。我们说,正式将取代模拟和超卖和难度。

莎:这种情况在很多领域。你过分吹嘘为了得到投资。在一个我们的产品我们使用QBF(量化)布尔公式引擎来解决一个非常困难的问题。几年前,你不会考虑使用这个产品,但事情已经走到一个地方我们可以使用这些算法来让事情更有效率。引擎盖下,用户不需要知道正在运行。

女子你提出一个有趣的观点。波形已经非常接近我们传统上的模拟。人们理解它和他们写的规格。它是直观和建立。与正式的应用我们正在建设他们接近“正常”的世界里,和我的意思是它不是一个利基。正式属性验证仍然是一个利基市场,这就需要大量的专业的设计知识,在建模技术方面,抽象。建模的属性和刺激的约束真正需要的帮助工具才能成为成功的结果。低功率,疾控中心,连接应用程序——他们用户的生活简单。

福斯特:解决相关问题。

莎:我们已经收到客户的渗透应用意味着他们可以专注于他们的模拟在系统级的问题。这是一个重要的好处,并提供了关注点分离。仿真的优点是,它总是返回回到你和设计提供了一些见解。正式的,在过去,是作为一个端到端的,自动化的解决方案,该方案通过/失败。这是一个失败的秘诀,因为相关的理论极限可以走多远。但最近,发生了所有的工作,在过去的几年里,我们可以提供一些即使不是正式完成。当它所提供的结果是有界的信息报道,如果框架的验证信息是过度约束,甚至可以提供洞察设计。我们的每次运行的正式将提供可操作的回馈。这使它一样可以接受的模拟。很多工作也被投资于找出逻辑用于运行,这样可以报道报道。

福斯特:有另一件事。我们的人认为技术是互补的。我们在模拟使用正式帮助关闭覆盖。我们使用信息从模拟来帮助我们克服一些正式的状态爆炸问题。他们互相帮助,这不再是我们对他们。

女子:也许多年来它的发生,但是当我们谈论模拟,它本质上是不完整的。我们从来没有为我们设定了一个目标,在模拟实现100%的覆盖率。有一个实用的理论分别持股100%和100%。正式我们进了一个洞,我们认为它是全套盛装的签收。实际为100%,正式在哪里?覆盖是一个很好的例子,有界的结果使你得到一些的覆盖率,并捕获有限覆盖的可行的刺激将除了现有的模拟在系统水平。两个世界之间的交叉授粉可以实现更大的东西在系统级验证过程。

Montecillo:那是我们花了很多精力today-telling正式的团队有很多好处,增强仿真可以实现什么。我们从不说教,模拟将被正式取代。无论正式可以做一组是好的。写断言和他们可以可视化的方式使相反的例子。甚至不知道如何编写约束或假设,他们可以提供一些行为的语法和跟踪。这是强大的设计师。它与正式迈出第一步,然后他们开始写断言。一直有一种争论是否设计师应该写断言。我们觉得设计师写是最好的人,但是他们需要的动机。可视化,能够看到什么断言,他们有动机和利益开始滚雪球。 It is not all-or-nothing. Even a small investment in formal returns a huge benefit.