可以正式取代模拟?

一年前,Oski技术从来没有发生过的事情。它汇集了15最有思想的人形式验证部署和坐下来在一个房间里讨论他们面临的问题和问题和它们的方式试图解决这些问题。半导体工程记录事件。一年后,再次举行第二次正式峰会和半导体工程要求是墙上的苍蝇和捕获的本质的讨论。

为了促进自由交谈,参与者,下面列出,要求不被直接引用,所以所有评论转述,匿名的。

上图从左到右是戴夫•帕里Oski;Parimal Gaikwad Arteris;高通都Munishwar;Prashant Aggarwal Oski;Swapnajit Mitra,博通;朱赛义德·哈姆,英伟达,贾,AMD;Vigyan Singhal Oski;Anurag Agrawal,赤脚网络;Vikram Khosa却手臂;埃里克·塞利格曼,英特尔; Kaowen Liu, MediaTek; Roger Sabbagh, Oski; Viresh Paruthi, IBM; Naveed Zaman, Qualcomm; and Kamal Sekhon, Oski.

Oski技术的创始人和CEO,一开始用一个简短的历史。他说正式的验证已经从等价性检查,基本上比较一个逻辑锥与另一个用于每一个失败的设计。然后正式迁移到断言分析了锥的逻辑在几次失败。

“最近,我们看到公司成功与块级验证它取代的地方模拟并且可以实现彻底的验证,”辛格尔表示。“今天,我们正开始看到架构级形式验证可以帮助解决问题,如缓存一致性,没有死锁和块的互连。在未来它将不可能验证整个系统RT水平,我们将不得不解决他们潇洒地把问题分解,分解它。”

图1:从失败到系统。来源:Oski

Singhal指出,我们已经走过了漫长的道路,如今它成本100美元,和很多时间,芯片出了门。“我们变得懒惰,这可能是也可能不是一件好事,因为我们有依靠模拟太久。我们有时会忘记申请合适的工具。我看到人们试图解决一个高层次的系统验证问题,更好的解决了正式的,使用硬件模拟盒子。相反的情况也在正式应用于它不容易解决的问题。”

进化从失败到锥块系统产生不同的问题,和他们每个人都有自己的甜点。“因为我们依靠模拟这么长时间,我们已经忘记,随着设计变得更大,这正式达到块级和甜点知识产权验证。形式验证允许所有领导人的行业把责任回到它和应用正确的工具属于正确的问题”。

应用工程副总裁罗杰Sabbagh Oski,去年的一个参与者与华为时,此后加入Oski。架构验证是一个领域的前沿今天正式。”谁有经验与架构验证和你对它的看法是什么?”

“在当前的项目我们正在开发IP架构验证缓存一致性。你做不到这一点在顶层,因为正式的问题太复杂,”一位与会者说。“总有一天我们会到达那里。所以你必须分解问题。为每个组件创建一个架构模式,专注于你想要核实。你有多个此类组件缝合在一起,这样你就可以证明你的IP或协议。那你证明建筑模型对实际的RTL。最后一步是使模型在模拟。这个作品,使我们找到许多建筑和RTL问题。我们也将它应用到系统的其他部分有很多不同模块之间的交互。 The bugs found were difficult to recreate in simulation.”

另一个参与者看到架构验证等同协议验证。“你必须获得协议从一开始。就烤到流程和任何出现的新协议必须经过严格的验证。RTL的回接是不清楚。的跳棋架构级别上创建抽象模型,但对RTL扩展那些可以验证什么?”

有普遍的共识,这是有困难的领域之一,因为并不是所有对RTL可以得到验证。“大多数作品是用这样一种方式,我们可以证明他们对RTL。”

与困难的一部分抽象。抽象模型是RTL越近,就越容易。“我们将努力与建筑师时不要去想RTL建模。如果你这样做,你失去了抽象的好处。如果你不断担心你会创造更多RTL-like RTL模型和你失去的一些好处。这是一个平衡。”

他们看到的参与者有几种方法解决方案,包括这一个。“我们有肢解的架构模型,记住,我们要对RTL验证。确保有干净的定义良好的接口,该模型分解成块,将驯良的正式的工具和合理的刺激的约束和跳棋外围的街区。最后,我们很成功。逻辑部分的验证,我不知道在RTL的架构或发现的任何错误,所以它是非常有效的。”

并不是每个人都相信这或其普遍适用性。一个人得出的结论是,“我们不能把每个人都将架构验证变成RTL验证。我们可以利用它,但不能使RTL的终极目标。我们试图在架构级别验证设计问题后。”

其他参与者推迟。“关闭循环之间的建筑水平和RTL是很重要的。整个目标是验证在硅肉类生产是什么您的系统级需求。这是怎么做的?”

看来术语的共识。“这是困惑我为什么我们称之为架构验证?我们谈论的是一个系统,你定义一个新的协议和质疑的有效性协议和你没有RTL。该协议满足我的死锁条件吗?如果这是我们的目标,我不看到建筑进入它。如果我发展下一代的协议,为什么我在乎它如何实现?”

的一些分歧似乎回到架构是什么意思的区别和所使用的抽象。的人关注协议验证试图澄清。“当你在做架构验证,你可能会试图找出正确的消息序列的保证协议的性能。当它归结到RTL,您可以定义一些检查,但这更多的是一个实现检查。没有自动应用程序的抽象模型,得到直接应用验证。所以你带他们,但不是自动细化的方式。”

随着谈话的深入,好像有两个阵营。在一个阵营的人都定义体系结构和实现,而在另一阵营之间有一个分离那些定义的体系结构和实现。两组之间的这种变化信息如何流动和模型,可以提供。

第一阵营认为“抽象模型,用于架构验证,模型的一些行为或功能,必须真正的为了满足规范。你可能做出假设,然后实现它时,你必须证明这个假设是有效的。关闭循环。如果你能证明RTL满足,那么整个系统级的功能仍然是有效的。”

第二阵营在两组之间的差距。“这并不简单。你必须改进它。我们谈到传递的消息在抽象的层面,但在实现级别你正在谈论的消息的队列。有一个巨大的改进,进入他们。可以手工做一些改进,但这不是一个自动的过程。”

Sabbagh然后把对话引向一个新的问题。”我们应该用正式的bug狩猎或签收吗?优点和缺点是什么?”

第一个反应是“我们开始投资一些bug狩猎技巧。这已经被证明是相当成功的。缺点是没有明确指标所以很难衡量进展。”

参与者有问题的定义的签收意味着什么。一个试图提供一个定义。“这意味着我负责寻找每一个错误。如果你发现一个错误在子系统验证或模拟甚至硅,然后我希望有麻烦了。它可能是一个人类的错误。可能是我忘记包括检查器,但最好是一个答案。”

他们也分为正式和模拟的角色。“在我们的世界,块是一个更大的系统的一部分,那些需要用仿真验证。所以即使你可能开辟一块可以用正式的验证,事实是,端到端模拟还需要存在。所以我们不会就仿真工作。”

他们讨论如何实现正确的平衡。“这意味着有一个地方模拟技术可能是错误的。我们仍然要做的系统级仿真。洞被发现时,他们需要得到解决。作为一个例子,考虑一些仲裁逻辑位于织物。我们可以验证这个正式和证明它是正确的。端到端模拟需要存在,尽管我们可能已经验证了饥饿的正确性。带走的只有一部分从模拟也许几跳棋。”

似乎没有协议。“不管你底线在什么级别的层次结构,是块(或子系统)的水平,你正试图消除错误。如果你发现错误在更高的层面,做周后的伪constrained-random模拟,你应该问你能做些什么来改善验证在较低的水平。你会更好做块级模拟或块级正式验证找到这些bug和得到一个更强烈的信心,所有的bug被发现?”

“从项目管理的角度来看,当你说签收,我能承担什么?无论正式做一份好工作,应该是完全利用充分验证块。”

一个参与者试图与IP块。“想想看报道。你有一块硅验证的IP。现在合并成一个系统,你会验证该系统的工作原理,但您不需要测量覆盖在IP。你可以黑盒,你不必所有的角落案件。”

一些参与者不同意。“当你把它放到这个系统,你的职责是介绍依赖性在块级是不可见的。”

“但这意味着你有一个问题与你的约束。”

相当一部分的讨论围绕报道。“原因有覆盖率是衡量验证环境的力量。你不能扔掉覆盖从模拟环境因为你不会知道环境的力量。这些报道事件需要在仿真环境和保持活跃在正式环境中。”

”对我来说当我们说如果bug狩猎与验收,这是一个管理决策,而不是技术决定。是什么伤害任何块如果两个模拟和正式共存?它需要一个或另一个吗?”

大多数参与者观望。“当正式的适用性问题,你可能会摇摆模拟。但在正式更适用…一般来说,如果你正式和发现错误时,错误狩猎或指向签收吗?可能两者兼而有之。”

有几个反对这个,因为它暗示复制的努力。“你必须解决如何用固定的资源做事情。有正式的工作情况很好,是的有重叠模拟和正式的,但你不必gdp8 %正式模拟覆盖着。这是过分了。”

一个参与者试图澄清。“这是真正的单元级和系统级验证。我们有一个一般原则,你想找到每一个错误在尽可能低的水平,尽可能早的项目。我们说的是正式的强在单元级别。没有人认为正式在单元级借口你从做系统级验证。”

“你依赖于高水平的模拟与单位级验证发现问题!”

当话题转大圈回来签收的问题。“你所做的错误狩猎,直到没有缺陷。当时你在做什么?你还是要问:完整的足以被称为签收吗?为什么有一个或另一个吗?”

一个反应是:“这是一个连续体。你的目标验收开始,写一些属性和找到一些错误和增加,直到你有一个完整的属性集。但是你可能会遇到一个复杂的问题,…”

“这是一个项目时间表的问题。你不想在一个阶段你停止寻找bug,直到你完成你在做投资的抽象。你可以把证据进一步绑定并不断寻找漏洞的系统”。

结论似乎是一个出现在另一个。唯一的区别可能是最初的既定目标和跟踪目标完整性的质量。

有关的故事
高级合成究竟发生了什么变化?
已取得哪些进展高级合成在不久的将来我们能期待什么?
混合仿真逐渐升温
使用模拟和仿真的结合可以有利于一个SoC设计项目,但它并不总是一件容易的事情。
已取得哪些进展高级合成在不久的将来我们能期待什么?
正式的路线图(第1部分)
小组成员看正式的进展在过去的五年里,我们可以看到新功能出现。
故障模拟重生
一次不可或缺的工具是不同的应用程序卷土重来,但问题仍有待解决。
差距在验证流程(第3部分)
小组成员讨论软件验证,SystemC和未来技术将有助于验证跟上。