没有逻辑等价性检查,设计编译器可能永远都不会成功。是电子系统级(ESL)设计的成功依赖连续的等价性检查吗?
在第一部分圆桌会议,小组成员讨论了最近的变化,带来了正式的验证和讨论正式UVM带来的挑战。在第二部分小组专注于报道的主题和正式报道的方式可以结合模拟。在这部分,我们开始探索的影响顺序等价性检查将对设计实践。参与小组皮特荷迪,在节奏敏锐的正式产品管理总监;盎司Levia,营销和业务发展副总裁碧玉设计自动化,这是通过节奏;在真正的意图Pranav莎,首席技术官;营销总监戴夫•Kelf OneSpin解决方案;首席执行官和Vigyan Singhal Oski技术。以下是摘录的讨论。
SE:连续的等价性检查已取得哪些进展?这是一个必要的技术在ESL方法可以起飞?
Kelf:是的,这是一个必要的技术。高级合成(HLS)执行大量的顺序优化,和等价性检查必须跟上它的步伐。你需要什么东西,可以处理寄存器被移动。
Singhal:我们看到连续的等价性检查(SEC)被用于C和RTL设计之间的验证。这些主要是数据转换类型的设计,如无线基带或视频编解码器。所有这些参考C模型。肯定有一些限制,如不能无限循环,动态内存分配,等等,但我们能做到。
莎:我不认为你想这设定为一种到达月球的问题。你必须把这些问题分成小容易部分在空间或时间。实现SoC的一系列步骤。证交会应用于一个细化的步骤和时钟控制的一个例子。你之前和之后的步骤,您可以很容易地检查转换。
Levia:这里有几种类型的问题。首先是减少RTL和C是最复杂的问题。然后是RTL RTL的优化类型。即使在每一个有两个或两个以上的品种。有自动转换,然后手动转换或减少。可能有异步协议的引入,管道以等等。有很多小的改变会给发冷的RTL工程师如果他们回去验证使用基于仿真的验证套件。秒,用适当的映射,可以帮助他们收敛和说服自己功能的设计是相同的。正因为如此,我们看到爆炸的等价性检查。人们因为驱动的效率。
Singhal:是的,这就意味着他们可以更积极的优化。之前,他们可能是害怕改变的事情。
莎:一个很好的例子是如何初始化一个电路。一个简单的方法是将在每个时钟异步复位。这可以检查结构很容易。但是如果你有一个工具,可以检查更复杂的重置计划,然后你可以节省电力,节省资源布局。
Levia:它是开放的视野,人们没有想象。我是一个高级合成时更加怀疑。设计师将分为两个阵营。他们会认为HLS是好的或者,像设计编译器,他们不会相信它是正确的。我不认为SEC将从根本上改变他们如何看到HLS。
荷迪:每个人仍然不相信设计编译器,使用等价性检查。
Kelf具体问题:这是一个问题。与数据路径,很多人正在使用HLS并信任它。一个问题是他们是否能可视化结果。这是问题的一部分设计编译器。当一个工程师有一个好的感觉出来什么与什么进去,然后他们开始使用合成。
莎:证券交易委员会使HLS。但更重要的是需要能够断言RTL和地图回到C描述。也是如此的覆盖漏洞。你需要地图的事情回到一个高层次的描述。
SE:很明显,整个设计永远不会通过HLS美联储,但将大量的集成块。我们如何验证这些设计?
荷迪:我们还没有谈到的是连接,如果我们看看SoC水平连接,模拟是低效的。正式的很好。这也许是最激增的正式应用。
Singhal:设计IP的交货有问题,这是与质量。我们现在在舞台上的正式设计IP可以完全证实。我们需要他们提供的阶段IP和一个完整的正式证明可以在客户站点上重播。如果我给你的权利来修改RTL那么证明可以重播。到目前为止,设计IP公司投资不够正式。
Levia:以正式从单位子系统和系统,连接是一种类型的应用程序,它到处存在,从最低mux连接功能连接。另一个应用程序是寄存器映射。在几乎每一个级别的设计需要确认或寄存器访问的内存做正确。建筑规范是另一个。如果你有一个规范的长达500页的东西,你需要找到一个方法来形式化,然后很容易开始寻找内部问题,冲突,死锁等。正式的瑞士军刀。有很多东西你可以用它做,几乎每个季度,有人发现一种新的方式使用这项技术。
莎:块之间的连通性,对寄存器是如何连接的,都是关于你如何把事情放在一起,而不是里面有什么。低挂水果这里是能够推断出所有的自动检查你所要做的。UVM可以帮助。这个行业需要思考如何指定诸如协议,这样就可以开采提取验证义务。
Kelf:有趣的是,每次我们先说机会是在模拟的问题,和连接就是其中之一。当我们得到更多的阻塞是相互关联的,被束缚的规模,那么也许我们可以更有效地应用正式比模拟更大比例的问题,随着时间的推移,模拟将开始推出。这是未来。
Singhal:正式已经走过了漫长的道路,但需要的方法,你必须注意你的组织,金字塔你建立公司内部的专家,并确保你给他们正确的训练和方法和工具。这是赛车车完全一样。你可以给他们最好的技术,但你必须训练他们能够使用它。
|
|
|
|
|
|
|
|
|
|
[…]正式准备好取代模拟吗?没有逻辑等价性检查,设计编译器可能永远都不会成功。是电子系统级(ESL)设计的成功依赖连续的等价性检查吗?[…]
[…]正式准备好取代模拟吗?[…]