正式的新面孔

半导体工程坐下来讨论最近的增长与劳伦斯Loh采用正式的技术和工具,产品工程组主任节奏高级经理Praveen女子,研发、验证小组Synopsys对此哈里•福斯特首席科学家导师图形,Normando Montecillo副技术总监博通公司和Pranav莎,首席技术官真正的意图。在第一部分,小组成员讨论了导致的增加的变化采用和持续的可能性。下面摘录,谈话。本文的第一部分,点击在这里。

SE:使用正式的成长?

莎:人们传统上认为正式的一件事,但是它有两个重要的部分。一是规范方面,另一个是分析。人俱乐部在一起,但他们是不同的,只是用正式的规范有一个好处。有艾滋病写作断言,这是更容易但SoC的额外层创建自己的抵押品,如环境,重置,dft, UPF值。也有公司帮你捕获寄存器的设计信息。这是被写入抵押品帮助芯片的设计,你可以提取大量的断言的抵押品。这意味着大量的一部分你需要的信息隐含在设计描述本身还有其他隐式的RTL。艾滋病对于正式断言写作进展更容易和有很多隐含的断言。这些帮助简化规范的一部分。为分析,它可以被认为是更复杂的模拟。 Those algorithms have been worked on for a number of years and combined they provide a complete solution.

Loh:我看到的是不同的。最流行的应用是正式产权验证到目前为止。为什么人们说这是很难使用当我们不看到了吗?我意识到正式属性验证(废票)不仅仅是一个正式的专家运行一个棘手的问题。这并不是大多数使用。它不是关于验证是正确的,它是关于找到一个反例,看到动作的设计。给我一个想法,我需要写检查并提供一种验证团队选择设计师的大脑使用正式的说明什么设计。也许是设计师试图表明验证规划工具。

福斯特:我不认为我们不同意的状况。关键是当使用废票有两种使用模式和错误狩猎和保证。他们是完全不同的,保证需要大量的专业知识如何写我如何创建抽象属性。现在虫子狩猎,为设计师有很多价值写断言是否发现bug。困难的是如何量化这种回报是什么呢?这是一个管理问题,表明我们已经生产通过使用正式的属性检查。

Loh:是的,bug狩猎是一个主要的使用模型。正式的,根据我的经验,所以更快和更早的能找到bug。让我的基础上保证的部分。传统上如果你有一个完整的证明是好的,但是如果你没有得到一个完整的证明你没有得到任何可测量的保证。我一直在试图避开。一个完整的证据并不是唯一的办法保证和我们努力获得准确的可见性验证,用周期边界定义,这组。我们需要一种方法,人们可以理解,这是密切相关如何测量模拟覆盖。正式的不相同,但他们可以并排和参考验证计划。

福斯特这是重要的。设计工程师可以做分析和实现,如果我做50个周期,这将是足够的,将覆盖一切。可能仍然有风险但有技术求出边界。通常,处理器的家伙一直在做的有界模型检查和达到足够的信心。

女子:我明白,设计师们最能写断言,但错误在哪里?他们大部分时间发生当两个街区相互作用。你可以背压,你可以流水线,复杂的场景,不能很容易想到。正式的美妙之处在于,这些场景可以提取。现在你怎么那么快,没有充分理解设计?它就像一个点名,有人说50周期对我来说已经足够了。也许这是55或52。我们如何来一个完整的解决方案吗?有很多分析技术帮助用户,但它仍然需要一些设计知识。它不是一个验证活动。 It requires designer driven analysis to come up with the right bound. One of the benefits of formal is that it makes the designers and verification engineer become a lot closer. They have to interact. This is a good synergy.

Loh除了一件事情:我同意。设计师将有一个受过教育的猜测,如果是50或60。报道也一样。好的验证工程师应该能够考虑所有的角落病例或评审测试计划并决定这空缺需要填补但这是好的。该工具应该能够帮助他们实现。在正式,如果他们说五十是好的,如果该工具可以告诉它涵盖逻辑智慧和五十人会添加这个额外的,如果它不提供任何额外的,那么这是很高兴知道。在一天结束的时候,设计师还需要签字。

莎:正式成为可行的,并提供了下一步要做的事情。

福斯特:这是一个早期的技术和工具的问题,使得用户的负担来找出什么是可行的,什么是下一步。

女子:把一个科学计算器。你把它给一个人,让他们来解决,但是你还没有告诉他如果是一个微分方程或微积分。你去弄明白。但是正式的进化技术现在有指导,可以帮助他们找出方法。更多的分析技术,提取属性是帮助用户去思考他们的设计以及验证的领域。

SE:正式的能做什么来帮助愈发担心安全吗?它可以用来识别攻击吗?

福斯特:我们都提供一个安全的应用程序,但现实是,如果你有一个明确的问题很容易想出一个正式的解决方案。安全的问题是,它是一个巨大的领域和解决所有已知的问题不容易处理的。有许多可以解决。你可以保护某些寄存器,只有人正确的凭证可以访问作为一个例子。

莎:就像在SoC设计中,有两种类型的故障领域的安全。一个是一个实现由用户错误和语义分析的代码将帮助你找到它。期待正式能够处理复杂的协议和告诉你如果正确实现是一个困难的问题,将设置期望过高期待正式能够解决这个问题。

福斯特:这是看作为一个架构和一个实现角度。您可以使用正式的,但建筑往往意味着定理证明。

女子:如果问题是全球的性质,这样从a点到b点没有数据流,应该可以与形式分析建模和检查。但并发症出现,当管道需要检查系统中某些事情无法改变。这变得复杂,因为有一个软件角度。在低功率,如果软件和硬件实现的低功耗方案是被动的,这是大多数系统的方式,很难验证,因为真正的智能软件,而不是硬件。你真的能做什么样的形式分析的硬件?这样做需要大量的建模软件的意图,进而带来另一个挑战,如何验证软件,目的是完全一样的吗?这是提高抽象层次,对体系结构验证,而不是硬件验证。

Montecillo:我们的很多安全是嵌入在硬件本身,所以这个问题很简单。我们有一个或多个部分,我们不想泄漏任何条件下除了定义的场景。这对我们来说是非常困难的描述甚至在今天的模拟。我们需要一个新的语言,将使我们能够描述这种行为。我们今天没有好的解决方案。我们所做的大部分工作是基于模拟。

Loh:安全应用程序已经存在好几年了,但它不是一个单一的问题,它是一个类的问题。它是一样的说,‘我希望我的芯片工作。我们可以有正式这样做吗?“问”,我的系统安全吗?”并不是一个定义的问题。每个人都必须做好自己的部分,硬件和软件,握手要定义良好的,不妥协,和软件需要有一个良好的加密算法。有许多事情发生。选择的部分,你可以提供一个解决方案。确保一个安全登记不得访问。弄清楚在软件规范,这是一个软件要求必须在软件验证,否则系统是不安全的。安全是人们不喜欢讨论在一个开放的论坛,和公司不想谈论他们是如何验证安全,因为你说的越多,你越可能显示你的弱点。 Customers often don’t want to tell us what they are doing.

莎:如果你限制的范围你解决安全问题,如定义特权和非特权的部分芯片,复杂但范围较窄,看起来就像许多其他应用程序。但是有一个警告如果有软件参与系统。

福斯特:这是我的意思通过设置正确的预期。如果你只是说正式可以解决安全问题,那么将创建问题。我的背景是等价性检查和回“90年代人问道:“这是奔腾吗?证明等价!”

SE:确保供应链是另一个相关的区域。你怎么能确定一个木马已经插在设计?等价性检查是一个好的工具吗?

福斯特:有很多技术被探索。如果我做一个芯片,寄给工厂,我可以看看一些恶意已经插入?一种想法是寻找一个电压或功率不同于我们所期望的事情。你正在寻找差异为特征的设计和芯片,回来看到如果不以预期的方式表现。等价性检查并不是简单的你什么时候回来大量的晶体管。

女子:它取决于在哪里以及如何插入。对于任何插入它,他们必须聪明,所以它可能不容易观察到的。

福斯特:美国国防部高级研究计划局正在花很多钱到这个它应该帮助。

莎:它通常可以融合将引发特洛伊的许多事情,这是一个很难解决的问题。

Loh就是这样黑客似乎总是领先。

莎:电压和电流数据挖掘的一种方法。有一个公司,分析了芯片的射频输出,如果有可以利用的地方,然后你可以了解发生了什么事情在芯片内基于这个概要文件。所以你可以描述一个已知的芯片,然后比较好。

福斯特:真的外来技术正在探索解决这一问题,许多不属于正式的域。