成功应用形式化分析的十大技巧（三）

路科验证 2021-07-15 13:08

【50份好礼】首发直播：解密Keysight最新模拟信号源 【有奖直播】提升毫米波信号测试精度

这是在IP和SoC项目中成功使用形式分析的“十大技巧”的系列文章中的最后一篇。作为提醒，这里列出了第一期和第二期中涉及的六个技巧：

技巧1：让设计师参与属性的定义，并尽可能进行形式分析
技巧2：在项目早期进行形式化分析，以便定义属性的工程师立即受益
技巧3：利用从基础设计检查器到断言综合的所有形式的自动断言
技巧4：标准协议，尤其是片上总线，要利用基于断言的IP（ABVIP）
技巧5：利用形式化的“应用程序”，例如高度多路复用SoC引脚的连接检查
技巧6：认识到形式分析对于证明断言以及发现设计和规范错误的价值

上一篇文章以融合形式分析和模拟结果为主题进行了讨论。由于验证主管和项目经理习惯于基于模拟来评估进度，因此，最合乎逻辑的方法是将形式化结果转换为模拟验证的术语。这就需要扩展报告的结果以包括经过验证的断言。模拟验证本身不能生成证明，但可以从形式分析的证明中受益。尽管不建议这样做，但是用户可以选择在模拟验证中禁用任何被形式验证证明是“安全”的断言。

从断言转移到覆盖范围，含有无法触及的覆盖范围是经过验证的断言存在的必然结果。当形式分析证明一个断言时，它从数学上确定从输入（在输入假设的范围之内）不存在违反该断言的合法路径。同样，一个无法触及的覆盖就是从输入到该覆盖点没有任何路径。主要的区别是不可达性分析时，只需很少的输入假设下即可完成；如果在没有任何假设的情况下无法覆盖，则覆盖点也将无法覆盖。这将引出以下的技巧：

技巧7：使用形式分析来检查不可达的覆盖点，以提高模拟验证的覆盖结果

模拟验证没有不可到达性的概念，因此IP和SoC项目团队通常会花费大量时间和精力来尝试可能无法到达的覆盖点。形式分析可以分析PSL和SVA的覆盖属性，并且可能发现其中某些实际上是无法触及的。将这些结果与模拟验证结合起来非常有用，因为它会向验证团队发出信号，告知他们应该停止尝试命中这些覆盖点，而是检查为什么它们无法触及。这种分析可能会发现设计错误，例如设计的一部分被隔离掉了。

在Cadence®度量驱动的验证（metric-driven verification，MDV）流程中，可以通过形式化分析和模拟验证来处理常见类型的代码覆盖率。这些无法到达的结果特别有价值，因为大多数项目在签核时更多地依赖于代码覆盖率，而不是PSL/SVA覆盖率。与覆盖属性一样，验证工程师不应简单地放弃无法覆盖的代码覆盖范围。相反，他们应该分析每个覆盖点，以确保它确实不可触及，而不是设计错误的征兆。

飞思卡尔半导体公司最近的一篇论文描述了他们的验证团队如何在Cadence MDV流程中使用代码覆盖率不可达性的分析来确定应从报告结果中“排除”的覆盖率。[1]这使得团队可以更快地实现覆盖收敛，并在设计者批准后删除“死代码”。飞思卡尔团队还使用形式分析来达到他们尚未在仿真中达到的覆盖率。

技巧8：使用形式化分析，通过展示如何达到难以触及的覆盖点来帮助覆盖率收敛

使用形式分析来解决覆盖点的不可达性自然会引发一个问题，即形式化技术是否可以帮助命中可到达的覆盖点。实际上，形式分析可以像声明一样针对覆盖点，尝试从输入（在输入假设的范围内）生成一条到达覆盖点的路径。许多形式工具可以直接针对基于PSL和SVA覆盖属性。其他功能（如Cadence MDV流程中的功能）也可以定位代码覆盖点。无论哪种情况，都可以将形式化的结果与模拟验证的结果结合起来。

验证团队通常会考虑使用形式化分析来尝试达到模拟验证中未达到的覆盖点，通常是在项目后期。当SoC或IP团队“努力工作”试图命中未执行的覆盖点时，其中某些覆盖点可能是不可达的，而另一些则可能难以触及。无论哪种方式，形式分析通常都能提供答案。但是，没有必要非得等到项目后期。一些团队甚至在没有模拟测试平台之前就使用形式化分析来达到项目早期的覆盖率。

确定覆盖点不可达与使用形式分析命中覆盖点之间存在一个重要区别。后者需要一套合理完整的输入假设，因为以非法输入序列达成覆盖点并不公平。命中一个断言或一个覆盖点通常需要输入假设，而证明断言或确定覆盖范围不可达性通常是用最少的假设完成的。对于形式工具，断言和覆盖点在概念上非常相似。

就像无法总是命中或证明复杂设计中的复杂断言一样，有时形式化分析既不会触及覆盖点也无法证明其无法实现。如果模拟验证恰好遵循正确的路径，那么可能会命中对于形式分析而言过于复杂的断言或覆盖点。在实践中，这不是很常见，除非确实是在触及形式化算法容量极限的超大型设计上。在某些情况下，可以通过结合使用形式分析和模拟验证来获得最佳结果。

最常见的“双引擎”技术是使用仿真为形式分析设置一个有趣的起点，而不是从重置开始。一些形式工具可以从仿真中读取轨迹文件，并在开始分析之前初始化为模拟运行中达到的状态。一个典型的例子是具有较大深度的FIFO设计和“ FIFO已满”覆盖点。容量限制可能会妨碍形式分析从复位生成填满FIFO并命中覆盖点的路径。

运行一个模拟验证的testcase，使得FIFO已经被大量填充并在此时开始形式化分析可能会更成功。对于与“ FIFO已满”条件有关的断言，例如，FIFO永远不会溢出（即，在已满时接受写操作）并丢失数据，这种技术尤其有用。请注意，从非复位状态开始通常对于证明断言或确定不可覆盖范围无效，因为这需要分析复位后所有可能的行为。

Cadence的MDV流程提供了其他形式的“双引擎”操作，这些操作可以帮助达成断言，并涵盖仅凭模拟验证或形式分析都难以实现的断言。其中最有价值的是断言驱动的模拟，它把相同的输入假设用于形式分析，也用于生成模拟激励。如果在模拟中运行的结果路径命中断言或覆盖点，则用户会知道这是有效的，因为仅应用了合法的输入激励（在输入假设的范围内）。

断言驱动的模拟为人们提供了新的验证可能性，尤其是对于那些设计者可以：

在任何测试平台可用之前，在其模块上运行模拟测试
发现违反断言的早期错误
查找经过验证的断言和无法触及的覆盖点
根据生成的路径优化输入假设
了解有关另一个项目中重复使用的陌生模块

NVIDIA最近的一篇论文讨论了在复杂的多级内存控制器上使用断言驱动的模拟。[2]这项独特的技术使NVIDIA团队可以为设计制定适当的输入假设，确定要进行正式分析的“最佳位置”，并在开发过程的早期发现有趣的设计错误。可能发现的最有趣的错误是在一种情况下，即使没有请求，客户端也被授予了内存访问权限。

技巧10：使用形式分析来追踪硅后bug的来源，可以通过断言来捕获这些错误的影响

尽管形式分析通常用于硅前验证，但它对于实验室中发现的某些特定种类的错误也起着非常重要的作用。硬件错误的影响可能会在系统级别出现，例如程序崩溃时。如果初试工程师可以将错误影响缩小到可以用断言描述的错误行为，那么可以进行形式分析以找到可能违反断言的路径。这种方法可以在实验室中尝试使用逻辑分析仪查找硅后错误的源头，从而节省数天或数周的时间。

本系列文章介绍了10个技巧，这些技巧可以用来提高形式分析的成功率。对于经验丰富的形式分析用户而言，某些技巧可能是显而易见的，但对新手而言则不是。通过遵循这些规则，新用户和现有用户都可以从他们的工具中获得更好的结果，充分利用他们的投资，同时获得只有形式分析才能提供的确定性和完整性。欢迎任何意见或者其他技巧的建议。行业中有很多成功的形式化方法应用，共享最佳实践可以使所有人受益。

References 参考资料

[1] “Innovative Approach to Coverage Closure Through Un-Reachability Analysis Flow” by Ashish Goel, Tejbal Prasad, and Abhinav Nawal, CDNLive! India 2011, http://www.cadence.com/cdnlive/in/2011/pages/proceedingssummary.aspx

[2] “IP Verification Methodology Using Property-Driven Simulation in Incisive Enterprise Verifier” by Deepanjan Roy, Abhishek Datta, and Lokesh Babu Pundreeka, CDNLive! India 2011, http://www.cadence.com/cdnlive/in/2011/pages/proceedingssummary.aspx

往期回顾：

成功应用形式化分析的十大技巧（一）

成功应用形式化分析的十大技巧（二）

原文链接：https://www.eetimes.com/top-10-tips-for-success-with-formal-analysis-part-3/

扫描上图二维码可直达课程页面，马上试听

新一期的路科验证V2Pro秋季班报名通道已开启！对于课程学习有任何问题，都可以扫描二维码联系路科验证MOMO。
👇课程详情👇
嘿，想拥有“招之即战”的能力么？验证V2Pro秋季班等你加入！
❞

往期精彩：

除了这门升级中的V2Pro课程，恐怕你找不到更好的学验证的途径了

在V2Pro春季班开班前，你是否还在疑虑这些问题？

路科发布| 稳中带涨！25w成芯片校招薪资平均底！2020应届秋招数据全面分析！

相约今晚8点社招转岗有顾虑？成功上岸的同学来帮你

UVM RAL模型：用法和应用

如果你突然被裁员了，你的Plan B是什么？

[彩虹糖带你入门UVM]

理解UVM-1.2到IEEE1800.2的变化，掌握这3点就够

登录阅读全文



免责声明：该内容由专栏作者授权发布或作者转载，目的在于传递更多信息，并不代表本网赞同其观点，本站亦不保证或承诺内容真实性等。若内容或图片侵犯您的权益，请及时联系本站删除。侵权投诉联系： nick.zong@aspencore.com！

路科验证专注于数字芯片验证的系统思想和前沿工程领域。路桑是Intel资深验证专家，主持验证架构规划和方法学研究，担任过亿门级通信芯片的验证经理角色。在工程领域之外，他在西安电子科技大学和西安交通大学客座讲授芯片验证课程。著有书籍《芯片验证漫游指南》。

进入专栏

文章：1050篇粉丝：51人

 私信

成功应用形式化分析的十大技巧（三）

最近文章

热门文章

推荐

最新资讯