rockeric.com

形式验证的领导者们正在讨论扩展形式验证工具的方式，以最大限度的解决日益增加的任务。

一年前，Oski Technology做了一件从未发生过的事情，它召集了15位形式验证方面的顶尖专家，坐下来讨论他们正在面临的问题以及试图解决这些问题的方式，Semiconductor Engineering记录了这次讨论。一年后他们进行了第二次交流，Semiconductor Engineering同样记录了讨论的精髓。

为了促进以后更自由的讨论，下列参与者的意见并没有被直接引用，而是以解释阐述的方式展现，有些观点匿名展现。

从左往右分别是： Dave Parry，Oski；Parimal Gaikwad，Arteris；Mandar Munishwar，Qualcomm；Prashant Aggarwal，Oski；Swapnajit Mitra，Broadcom；Syed Suhaib，NVIDIA；Jia Zhu，AMD；Vigyan Singhal，Oski；Anurag Agrawal，Barefoot Networks；Vikram Khosa，ARM；Erik Seligman，Intel；Kaowen Liu，MediaTek；Roger Sabbagh，Oski； Viresh Paruthi，IBM； Naveed Zaman，Qualcomm；Kamal Sekhon，Oski。

---

形式验证在系统架构验证的方案

Oski Technologies首席执行官兼创始人Vigyan Singhal从一段简短的历史开始了阐述。他表示形式验证是从等价性检验发展而来的，最基本的功能是通过设计每一个寄存器来对比两个逻辑锥。后来形式验证兼容了断言，可以通过一组寄存器来分析一系列的逻辑描述。

Singhal说：“最近，我们看到公司在模块级验证方面取得了成功，它取代了仿真验证并可以实现彻底的验证。” “现在我们开始着手架构级的形式验证，它可以帮助解决诸如缓存一致性，无死锁和模块互连等问题。将来不可能在寄存器级别验证整个系统，我们必须将这个问题巧妙的进行分解，然后解决。”

（图1：从寄存器到系统。来自：Oski）

Singhal指出，我们已经走过了很长的一段路，至今已经花费了1亿美元，并且花了很多时间让芯片走向市场。“我们可以更加懒惰，这可能是一件好事也可能不是，我们已经依赖于仿真验证太久了。我们有时候忘了为这个工作选择一个正确的工具，我看到有些人试图解决一些更高层级的验证问题，当这些问题更适合用形式验证解决，他们却使用了硬件模拟（hardware emulation）；而当形式验证无法解决问题时，他们却依旧选择了形式验证。”

从寄存器到逻辑堆再到模块进而到系统级，出现过各种各样的问题，并且每个问题都有各自最佳的解决方式。“因为我们长时间依赖于仿真验证，我们已经忘了随着设计变得越来越大，形式验证在模块级别以及IP的验证上已经达到了解决问题的最佳时刻。形式验证可以帮助行业中的领导们把责任推回到问题所属的模块，并使用正确的工具来解决问题。”

Oski应用工程副总裁Roger Sabbagh去年作为参与者时还在华为工作，后来加入了Oski。架构级别的验证是当今形式验证的尖端领域之一。“有没有人掌握了架构验证的经验，你们是如何看待这件事的呢？”

“在目前的项目中，我们正在开发用于缓存一致性架构验证的IP。你不能在顶层做到这一点，因为这个问题对于形式来说太复杂了”，一位与会者说。“有一天我们也许能够做到，但目前你不得不分解这个问题。对于每一个组件，你都需要创建一个架构模型，来专注于你要验证的内容。你有好多个这样的组件，并将它们集成到一起，使其能够证明你要验证的IP或协议。然后你再证明这个架构模型与实际的RTL是否相违背，最后一步是在仿真中启动模型。这种方法起到了作用，让我发现了许多架构和RTL上的问题。我们也将这种方法用到系统中有很多交互部分的模块上，发现了一些很难在仿真中重现的缺陷。”

另一位与会者将架构验证看作协议验证。“你必须从一开始就拿到协议，它会被应用到开发流程中，任何伴随该协议新出现的协议都必须经过严格的验证。但是RTL的实现我们并不清楚，这些协议的检查器是在架构级的抽象模型中创建的，但是该如何保证这些检查器对RTL得到充分的验证呢？”

普遍的共识是：这是困难的领域之一。因为并不是所有事情都可以在RTL上进行验证。“大部分检查器以可以在RTL上进行验证的方式被完成。”

这个问题的一些困难与抽象有关，抽象模型越接近RTL，它越容易做成功。“我们强烈建议设计师在建立抽象模型时不要考虑RTL。如果你这样做，你会丧失抽象的好处。如果你不得不考虑RTL，你会倾向建立更多类似于RTL的模型。虽然RTL模型方便建立但又失去了一些抽象模型的好处，这是一个需要平衡的事情。”

参与者提出了一些可行解决方案，这是其中一个。“我们不得不分割架构模型，时刻记着我们想要通过模型来验证出RTL的反例。确保接口的定义清晰，将模型分解成更利于形式验证的块，并在这些块的外围添加合理的激励约束和检查器。最后我们很成功。对于已验证的逻辑部分，我们没有在架构模型或者RTL中再次发现任何的缺陷，所以这非常有效。”

但不是每个人都信服这个方法或这个方法的普遍适用性。一位与会者总结道：“我们不能推动每个人将架构验证转化为RTL验证。我们在可以的时候使用这种方法，但不能使RTL验证成为最终的目标。我们正试图在架构层面进行验证，以解决后续的设计问题。”

其他参与者提出了意见。“关闭架构级和RTL之间的循环非常重要。整个目标是验证硅上的产品是否满足系统级要求。那应该怎么做呢？”

看来，一个术语正在成为焦点。“我感到困惑的是，为什么我们称之为架构验证？我们正在讨论一个系统，在这个系统中，你正在定义一个新的协议，并且质疑协议的合法性，但又没有RTL。这个协议是否满足死锁条件？如果这是目标，我看不到架构如何加入它。如果我们正在开发下一代协议，为什么要去关心它是如何实现的？”

一些分歧似乎回到了架构意味着什么和抽象的使用上。专注于协议验证的人试图这样区分。 “当你进行架构验证时，可能试图从保证协议属性的角度来发出正确的消息序列。当对RTL进行验证时，你会定义架构模型中一些检查器，但这更多的是用来进行检查。这些检查器不会自动对你直接应用到抽象模型上的验证内容进行处理。基本上是你在不断改进它们，而不以是一种自动改进的方式。

随着对话的进展，似乎存在两个阵营。在一个阵营中，包括了既定义架构又使用它的人员。而在另一个阵营中，定义架构的人员与使用它的人员分离开来，这使得两组人之间的信息流动和提供的模型发生了变化。

第一个阵营认为“用于架构验证的抽象模型包含了一些行为或特征，它们一定符合协议规范。可能先做出了一些假设，然后对其进行验证，你必须证明这些假设导致的结果是正确的，这样就关闭了循环。只要你再能证明RTL也符合要求，那么整个系统级功能依旧正确。”

第二个阵营纠结于两组人员之间的隔阂。“这并不是那么简单，你必须改进抽象模型。如果在抽象级别上信息的传递发生了变化，那么在实现它的层面上就需要考虑这些包含信息的队列。有大量的改进加入到协议中，所以你必须手动的进行一些修改，这不是一个自动的过程。”