验证统一

半导体工程汇集了行业名人发起讨论正式技术将扮演的角色与最近发布的早期采用者的草案的便携式刺激以及它如何有助于拉近两种执行技术。参与这个圆桌会议是乔Hupcey,验证产品技术专家导师,西门子业务;验证的传道者,导师和副主席汤姆•菲茨帕特里克的便携式刺激工作组(PSWG);的首席执行官Breker;工程副总裁罗杰Sabbagh应用程序Oski技术;肖恩·Safarpour CAE主任VC正式Synopsys对此;汤姆·安德森,他是产品经理节奏时间和秘书的便携式刺激工作组;和Ashish Darbari,产品管理主管OneSpin解决方案。第一部分可以被发现在这里,第二部分在这里。下面摘录,谈话。

SE:迄今为止对话功能。还有其他事情要担心这些天。是什么权力吗?

菲茨帕特里克:有两个方面。一个是电源控制器,我们展示了如何处理的一部分,在DVCon教程。它就变成了另一组设计中指定的操作。这只是另一个方面的刺激设计成一定的权力状态。还有的问题建模首先使用的功率控制权力统一格式。如何变得更模拟器模型。有一些额外的映射,把设计之间会发生在这个电源状态,这实际上是如何实现的。

Darbari:你还没考虑到电源侧PS ?

菲茨帕特里克:是的,我们还没有考虑它是独立的。我们称它是刺激的另一个方面。

Darbari:这UPF值规范如何适应?我们怎么知道这两个是一致的?

菲茨帕特里克:UPF值允许您定义的不同权力的岛屿。我不会称它为一个意图的规范,但设计规范。它成为设计的一部分测试意图方面,我们需要确保我可以打开和关闭电源,如果我试着做这个动作,然后这种力量岛最好是否则我不能这么做。我没有看到PS需要知道任何特定的UPF值以外的电源控制器算法,必须执行。

Darbari所以我们可以没有UPF值吗?如果我想检查它在系统级工作使用便携式刺激,然后我可以使用它没有UPF值吗?

Sabbagh:你想使用它的背景下趟车,因为你想要的权力结构的概念模型。

Hupcey:它是替代信息。

Sabbagh:你要模型在关闭这个东西,和这些孤立的细胞,这一块不能跟这一个。

Darbari:应该是独立于PS或扎成吗?

安德森:有很多事情你可以做形式验证低功耗分析的结构和控制,但概念是你想参加的考试从PS和叠加会发生什么当你开始改变电力领域。如果你打开和关闭的事情,做事情停止工作?我们往往发现关心这个的人是建筑师和他们有一个非常高级视图而不是UPF值。

SE:安全呢?

Safarpour:安全是一个领域,非常适用。客户感兴趣的正式的安全,因为正式的完整性。他们要检查安全架构级别的协议。我们不是在RTL在这一点上。最好的正式工具不能在RTL处理这个问题,所以我们在一些高级模型验证架构级安全协议。架构师可以使用PS的定义是什么,他将合适的模型来做,有什么值得信赖的成员,他们是如何允许访问安全的一部分内存,什么是不允许等正式可以验证模型。我们使用的是专用的输入格式今天要做到这一点,但它是一样的。

Darbari这需要一个synthesizable设计吗?

Safarpour:我们做一些建模。

菲茨帕特里克:某种高级RTL模型。

Sabbagh:你抽象的东西没有这个功能,所以您构建在本合同的建筑元素,模块或组件,你说我会认为这一块将做到这一点,你用RTL代码和模型假设和假设。

Hupcey:当你做一个安全的存储或路径的分析分析,这听起来像是另一个正式的情况分析和反馈PS。所以这是唯一途径进行反推装置,刹车的唯一路径或联锁或存储元素只有一个或两种方法读吗?都是正式的,一个特点是,可以导出一些情况刺激的约束或刺激在一个更大的图片,这将是由PS。一种技术可以最终确认,客户喜欢一些重叠和冗余——尤其是在系统水平。所以正式证明在RT级别,但我们想重用,学习在系统层面上,我们可以做更大的交易。

Safarpour:这可能是更重要的,因为正式的只是应用到模型中,不是RTL,所以当它进入模拟器,现在你真的可以用刺激来驱动它。

Sabbagh:我们可以关闭循环与RTL正式因为这些合约之间的阻塞,假设可以变成断言,然后当你得到RTL可以证明RTL符合合同。所以我和块匹配架构模型证明了建筑上的系统级属性模型,所以希望你得到相当高水平的信心。

哈米德:现在我们只需要从PS生成这些安全属性的抽象的RTL模型我们可以…

HupceyV:我们是遍历整个图。

SE:我们需要定义的路径图,是非法的吗?然后正式可以找到相反的例子。

Darbari:安全是典型的例子。故障模拟完成硬件设计上广泛,然后正式的出现和传播提供了评估分析。所以你可以注入和安全分析,但今天它是在硬件级别完成的而不是一个系统级。我相信人在软件会做同样的工作,但没有系统的安全。现在也许是一个很好的时间来捕捉这类问题。是需求,我们需要能够捕获在一个抽象的形式,这样我们可以推导出有趣的硬件和软件的测试。不是每个人都会去做系统级。硬件团队想做分析的硬件,和ISO 26262都有一个特定的任务。人们必须证明他们是兼容的。这里有工作需要。如何捕捉这在PS层吗?这是一个有趣的问题。

Hupcey:正式在一起非法和合法的利益,并证明硬币的两面。我很好奇在PS世界最佳实践可能是什么?你创建图表知道违法的情况下,确保设计拒绝他们喜欢它应该吗?

哈米德:绝对的。你有很好的情况下,你有错误的情况下,你有不做这个案例。

安德森人的安全方面,今天做的模型。处理器可以访问哪些内存区域或IOs是可以从哪些处理器。有某些事情,今天在PS模型。我们需要明白,生成测试。这可能是一个可编程寄存器的控制下。我不认为我们有解决整个问题。

SE:其他连接正式和PS之间存在什么?

Hupcey:报道是大的和客户每天都用这个。

菲茨帕特里克:我有了这个,因为我已经证明了它。

Hupcey:对,我还没有覆盖这个为什么不——因为配置。这就是人们采用技术将首先去。

DarbariPS:完整性是一个非常有趣的地方。如果你能pre-validate所有嘈杂的不一致的规范,它很有意义。这是最难的部分的验证和确认活动。无论如果你使用UVM和正式的,没人知道你是如何完成。然后你可能会有不一致的跳棋或约束,没关系的实际建模和如果在PS捕获需求,可以分析不一致,那是一个很好的特性,不存在其他任何地方。

菲茨帕特里克:我们设想的方式是有任何给定的要求操作,如资源。你有整个堆的事情和图我想做这个,然后说。工具计算出所需的所有其他东西从A到b可能有成千上万的方法。您可以生成一个测试和运行他们的全部或如果你能做一些分析图表,或基于一些外部分析…

Darbari:在规范或发现不一致。这是最大的吸引力。

Sabbagh:有点像正式规范的线头。所以如果你有约束和基于这些约束你的报道是遥不可及的,正式的能找到不一致或给定的图,你可能有一些死锁条件。

菲茨帕特里克:我们已经定义了语义,你能算出如果你想做一个紧随其后的是B,那么其他的东西存在在中间发生。在做,还有其他的事情可能会受到约束,这样它可以防止它被这些路径之一——这可能是一件好事。如果你写一个显式的场景中,我们可以说不,这是不可能的,因为这两个东西不能因为这个原因相互交谈。

Darbari:如果你有并发线程运行有一个顺序依赖关系,可能产生一个循环…

菲茨帕特里克:是的,它变得更加复杂,但对PS的另一件事是说我这堆东西的能力,你可以选择从。正式可以分析这堆东西…找出哪些实际存在。

Darbari所以你正在谈论的一致性和完整性。如果你没有一致性,那么你要担心。

菲茨帕特里克:今天,该工具可以识别一个永远不会被使用,因为它已被写错了,很容易找到。

Darbari:活锁将检查另一个有趣的事情。

菲茨帕特里克:那么问题就来了,我们目前做的事情我们能做一个RTL模型在PS模式和形式。

安德森:它是有趣的,我们一开始的道路上正式的PS能做什么。PS模式,如果你有一个正式的杠杆如何?我们已经转移到看着它反过来就是PS可以利用正式的可以提供的东西。

SE:涅槃能够设计和需求之间的等价性检查作为PS捕获模型?

Darbari:你不会总是完全等价,因为一个可以细化。

哈米德:你想证明设计的实现需求所定义的PS。

菲茨帕特里克:我不会坚持呼吸等待有人出来。

SE:那么,作为讨论的结果,将与PS不正式的人们开始参与?

安德森:尽管许多扩展领域讨论了PS,正式从来没有长大之前,它应该是。

菲茨帕特里克:同意。我们企业验证平台幻灯片显示四个引擎:模拟、仿真和正式的,我知道节奏有相同的图片。所以就好了如果我们可以说PS是他们所有人的层。

Safarpour:这个讨论很好但是我们做完这个后,我们回到日常和客户有一个块,他们正在与这些约束和他们都在问如何得到他们的证明,所以我们需要小步在短期内——它是什么,将提供足够的好处,如果我们喜欢正式和PS ?

SE:现在是时候这样做。一个小变化适应正式可以产生重大影响,使很多其他的事情。

菲茨帕特里克:第一步可能PS,也许从本教程并将其转化为一组断言,看看是否有意义。的问题将正式应用于PS模型更多的是一种工具的问题。每个供应商都有自己的方法。这不是标准的一部分。