为验证增加顺序和结构(上)

行业专家如何首次应对形式化能力成熟度模型。

你无法改善无法度量的内容，而在方法论方面，度量的概念变得更加困难。加入组织内个人的技能，能力和经验水平的概念，这可能会影响他们采用某些技术的能力，因此需要引起足够的重视。

这就是诸如能力成熟度模型（capability maturity models, CMMs）之类的概念开始发挥作用的地方。 CMM使公司可以评估其在技能和能力方面与行业内其他公司相比所处的位置，并确定可以优化的流程，以从其工程团队中获得更多价值的领域。它还可以定义与将新技术引入方法论相关的风险级别。

多年来，Wilson Research代表Mentor(西门子业务部门)进行了一项调查，以评估功能验证各个方面的行业成熟度。与任何调查一样，只有在调查中的问题保持不变时才能看到趋势。添加新问题或修改现有问题会破坏结果，因此花些时间才能看到这些新趋势。自调查开始以来，已发生重大变化的一个方面是形式验证的状态（见图1）。

图1. 形式验证技术的增长 资料来源：Mentor（西门子公司）

形式验证已从需要博士学位来理解并运用的技术，转化为更广泛的受众可以触及的技术。尽管添加了其他调查问题，但它们缺乏调查其他部分所见的深度和结构。例如，调查结果包括SoC集成连接性和X语义安全检查等应用程序，但不包括时钟域交叉。调查也没有说明如何有效地使用某些技术，例如基于声明的验证（ABV）。

建立成熟度模型是了解当今行业现状以便跟踪进度的第一步。这正是Oski Technology所做的，并于今年早些时候向行业专家小组展示了其第一个版本。Semiconductor Engineering应邀参加了揭幕仪式。为了促进自由讨论，所有评论都被匿名了，并提炼了参与者的主要思想。这次讨论的参与者是AMD的Wayne Yun；ARM的Ram Narayan； Arteris IP的Sanjay Deshpande；Ciena的Bryan Morris; Cisco的Anatoli Sokhatski; DE Shaw Research的Michael Theobald,; Google的Adriana Maggiore; Intel的Erik Seligman; Xilinx的Aniket Ponkshe. 来自Oski的Craig Shirley, Vigyan Singhal, Ninad Vartak, Roger Sabbagh和Gloria Nichols, LaunchM.

形式化的影响

形式化技术可以通过多种方式产生影响，但是每种技术的合理之处都不尽相同。重要的是，首先将它们与传统的基于模拟的验证流程相关联，以便可以评估收益。

图2 形式化验证对基于模拟的流程的影响资料来源：Oski Technology

许多公司都希望形式化解决仿真的弱点。“人们绘制这些曲线进行仿真，” Oski总裁兼首席执行官Craig Shirley说。“也许他们为模拟而绘制了这些曲线，但是他们没有为形式化而绘制这些曲线。形式化往往在这里显示出一点好处，或者在那儿显示出一点曲线变化，但是在某些方面它被归纳为一个不错的功能。今晚，我们将绘制一条曲线，显示各种形式验证方法对芯片级的影响。”

图2中的红色区域表示仿真较弱的地方。这样的区域之一就是基于测试平台的策略趋向于渐近水平，这使得团队难以提高覆盖率。有时，这是由于暴露这些错误所需的运行时间非常长。模拟有助于减少这些运行时间，但随后会给其他测试平台造成困难。

“好消息是这些错误中有90％或更多是模块级错误，” Shirley补充说。“它们不是系统级的错误。我们不断询问人们修改了多少模块来修复这些错误？它几乎总是一个。因此，即使我们将其称为系统级，我们仍在进行模块级验证。它们往往是高度平行的极端情况。”

这意味着仍有改进区块级验证的空间，而采用高级形式化方法的一种趋势是推动高风险区块的形式化签署。

图2中的另一个红色区域与首次发现错误的时间相关。开发基于仿真的测试平台需要花费很长时间，这意味着在第一个测试准备就绪之前就已经完成了许多RTL编码。 “当你开始早期使用形式化软件时，工程师通常会在漏洞创建后2或3天发现漏洞，” Shirley继续说道。 “ RTL在他们的脑海中仍然活跃。他们不必从其他项目进行上下文切换。另一个好处是，如果设计人员知道可以更快地发现错误并彻底验证其修正，则他们可能会更具攻击性。也许他们现在有更多带宽来修复错误，因为它们没有被错误淹没。你可能会在仿真中找到在这里发现的许多错误，但是最终你会更早地找到它们。”

One participant had an interesting perspective on this. “What shift left means to many people is how to get to mass cycles the fastest. How quickly can we be running on an emulator or FPGA? It is not just about the first bug. For me, time to last bug is more appealing than shift left.”

一位与会者对此有有趣的看法。“向左移动对很多人来说意味着如何最快地进入主循环。我们可以在仿真器或FPGA上运行多快？这不仅是第一个错误。对我而言，上一次发现错误的时间比向左移动更具吸引力。”

形式化级别

形式化的CMM定义了可以应用的五个级别的形式化方法。这五个级别都很有用，但是每个级别的目标，培训和工具要求都不同。从这次的讨论来看，将来很明显可能会增加其他级别，但这代表了当今的行业状况。

图3. 形式化应用级别。资料来源：Oski Technology

Oski应用工程副总裁Roger Sabbagh描述了图3所示的级别。“我们从级别1开始，人们在使用诸如自动检查的东西。这是非常基本的。自动形式检查集中在较小的特定问题上。你可能正在寻找超出范围的内存地址。用户甚至可能不知道他们正在运行形式化工具。无需编写任何断言。执行起来毫不费力。

“第2级介绍了形式应用。在这里，用户可以在电子表格中指定有关其设计意图的信息。例如，它们可以捕获设计中的所有连接，或者捕获不同类型的寄存器以及与那些寄存器关联的行为。该工具生成必要的断言。他们可能必须在设计的接口上应用一些约束，但是由于用户没有编写任何断言，因此采用起来仍然相对容易。例如连通性检查，门控时钟和顺序等效检查。

“第3级是人们开始编写分布在整个设计中的目标断言的地方。它们可能是由RTL设计人员编写的局部声明，例如，总线是独热总线。它们可以针对控制逻辑，例如仲裁器和FIFO控制器或接口。验证工程师可以在设计中添加断言，并且可以使用断言VIP，这可以检查标准接口协议。你可以对形式化验证中运用它们，也可以在仿真验证中运用它们。”

与第一级到第三级相关的大多数工具都属于左移类，这比使用仿真可能更早的发现错误。在讨论中，应该指出的是，其中一些工具还发现了在仿真中很难发现的错误（例如时钟域交叉），或者在仿真中可能花费很长时间才能发现的错误（例如连接检查）。

“第4级是我们开始代替模拟仿真，以进行模块级验证的地方，” Sabbagh说。 “目标是用形式化来签核模块的功能验证。这意味着正在开发的属性的类型会发生变化。他们成为端到端检查程序，而不是本地检查程序。形式化签核可以处理一些复杂的模块。例如，CPU的加载/存储单元，GPU的Warp定序器，网络设备中的多端口缓冲区管理器，PCIe接收器中的多通道对齐器或无线接口控制器的接收路径中的MAC级别块。

“第5级建立在第4级的基础上。我们开始进行体系结构的形式化验证，它解决了一些系统级要求，否则这些要求很难验证。我们可能会证明使用不同协议的多个异构CPU之间的缓存一致性。对于解决可能需要运行完整软件堆栈才能显示出问题的死锁的问题也是如此。”

级别1到3在很大程度上是由工具和语言解决的，但是级别3和级别4之间存在鸿沟。级别4需要更多的方法论上的贡献和更多的用户技能。此时，围绕公司内部包含的融合趋同和技能集的概念进行了一些讨论。达成协议的一个领域是，任何尝试达到4级或5级水平的公司都可能雇用全职的形式化验证工程师。

达到第4级需要技巧上的飞跃，但同时也带来不同的风险/回报级别。一位参与者评论说：“如果想让你的经理人投资形式化，那么进入第4级可能会更容易，因为形式化验证取代了仿真验证。在较低的级别上，当经理询问要哪些模拟验证可以省略或如何省钱时，你的答案是仍然必须运行所有这些仿真验证。因此，第4级实际上对管理层更具吸引力。但是，我不建议人们从4级开始，因为这样做是非常冒险的事情，会遇到很多麻烦。”

达成共识的另一个领域是级别的紧密度。 “级别1和2往往联系很紧密。第3级在每个设计中都会更改，以及第4级在每个项目中完全不同。较低的级别包含一大包的东西，可能对每个设计都有用，也可能没有用。但是，当你做一些事且奏效时，经理往往会很高兴并希望你重复一遍。”