正式的技术一直被认为是一个强大的验证工具。它是超越现在。
有更多的压力,使设计高效——从权力的角度来看,以及从一个整体设计视图——找到可以删除从设计更近一步。正如今天发表的文章中所讨论的,”我们可以减少从设计什么?”——序贯分析,基于正式的验证技术,正受到更多关注。
我特别要求导师图形工程总监,阿布Ranjan,形式验证技术是用于序列分析。
他解释说,起初,正是Calypto开始顺序形式验证。(导师图形在2015年收购了该公司。”公司的基础是建立在能够正式验证功能变化。在此之前,大多数的等价跳棋/正式的检查只是组合——他们将把失败边界视为神圣不可侵犯的,验证失败的范围内所做的更改。”他认为Calypto是唯一一家与技术验证顺序变化像re-timing re-pipelining,连续时钟门控,克隆和失败。
在业务过程中,Ranjan解释说,当设计来自客户的验证,导师的验证团队开始看到很多变化的能力,和设计团队正试图找出失败原因在边界情况下,额外的控制条件失败或记忆可以减少权力——和他们想要验证支持。虽然工具是能够验证这些变化,没有一个自动化的过程。
“我们认为,由于很多人是这样做,是有意义的自动化过程,和自动化的想法导致了序贯分析:发现您正式验证它的方式也可以用来生成这些限制条件。然后,我们走进一个序列分析发现路径冗余活动可以分析,”他说。
Ranjan补充说,真正的关键是,一旦你找出一种冗余可以分析,应用的范围,为各种其他类型的裁员变得无限,因为如果你能推理出任何redudant切换,无论是发生在时钟,失败,记忆,datapath公司——你可以几乎任何其他设计对象图。
有关的故事
差距在验证流(第3部分)
小组成员讨论软件验证,SystemC和未来技术将有助于验证跟上。
选择验证引擎
什么工具最适合一个特定的验证任务可能会更清晰的营销文献中比在现实世界中。
可以验证满足中间吗?(第2部分)
该行业长期以来认为验证是一个自下而上的过程,但现在有一个巨大的大力发展自上而下的验证标准。他们会满足舒适地在中间吗?
|
|
|
|
|
|
|
|
|
|
你好,安。有趣的讨论,但我觉得有必要指出一个错误的故事。在相等的使用顺序检查检查已经存在了一段时间,之前Calypto。OneSpin这项技术已经超过10年了,各种各样的等价性检查应用程序使用它。平心而论,节奏碧玉家伙甚至Synopsys对此也有很长一段时间。OneSpin也有SystemC前端的工具。导师,我相信,是最后一个市场,几乎第一!在这些天的特朗普我认为它重要事实吧!谢谢你,戴夫
你是绝对正确的,戴夫。我没有打算使它听起来像Calypto是唯一一个!谢谢你！