形式验证的潮流引领离不开这款工具

原创路科验证 2024-04-25 12:01

如何提升高压系统的实时性能? 精密双向电流传感放大器，提供精准测量，广泛应用于电流监测与保护

最近的时间，有幸参加了Simens OneSpin有关形式验证为期一天的会议，多数session我是跟了下来的，听了以后再次让我肯定了两件事情。一个是形式验证对于service的属性浓厚，需要围绕客户的需求、将形式验证四处开花，充分应用起来。另外一个是，Simens EDA这家公司一直秉承着他们创新探索的精神，很多EDA idea都能够从他们的工具早先让业界知道。整个一天下来让我受益挺多，会议先从行业境况、趋势，再到为了解决趋势当中的难点介绍OneSpin的新特性，继而有机会让听众了解到整个OneSpin是如何嵌入到Questa的功能验证family中。

接下来我将会议中一些让人有启发的PPT截取下来，将自己的理解和这些PPT结合起来，以便给路粉们对形式验证的一些新的发展方向有所了解。

这一张图还是相当直观有价值的，在左上角可以看到28nm制程和3nm制程不但是单次流片费用的急速上涨，而且还包括在这一过程中投入的用于验证（verfication/validation）和软件开发（software）的费用。可以看到，从28nm的验证费用$17M到3nm的$187M，整整上调了11倍（这个经费很离谱了..）。这张图也再次表明了，烧的钱都去哪里了。以7nm制程为例，验证（pre-silicon verification）的费用$47M仅次于软件开发费用$87M。

在过去的10年当中，项目中的验证人员数量增加了41%，但引起二次流片的设计缺陷还是增加了35%，这会引起对于验证投入策略的思考，尽管芯片复杂度提升和功能空间的爆炸确实需要人力的投入，不是说人力投入的多用处不够而是说这种投入按照常规仿真方法vs膨胀后的功能空间来看，其实还是“不够的”，依然有越来越多的功能bug在流片后外泄。所以在这个形式验证的会议里，自然地会提出一个问题——

是否不断增加的形式验证的投入并不会带来预期的结果呢？是不是应该考虑采取多样化的验证策略才能取得更好的结果呢？

一来是人力持续投入后的效果增长发力，二来是持续增加的复杂度，最后是全球性的IC人力短缺，不过不知道那个23,000的gap数字有没有包含国内的情况。在这种背景下，也就有了productivity gap（合理吧）。

这张图的比较也有实际意义的，它把静态验证拆分成了staitc和formal，而与simulation做了比较。static可以参考linting check，formal可以参考property check。PPT里的用词也很恰当，比如哪些情况属于“might exist”，哪些检查“with / without testbench”。这里formal与simulation比较起来，它的exponential与simulation linear特性比较起来，都做过这两种验证的同学就会深有体会了，在V3课程里，我们也将同一个design，同时采用formal和simulation做signoff verification，给了参考。面对设计的复杂度提升、传统仿真时覆盖率在80%左右时的缓慢爬坡，formal在这里的exponential就很有吸引力了。

如果遇到的设计本身要求验证的“completeness”，那么static & formal验证通过算法穷举的保证就可以确认这一点。之前谈到的仿真检查“linear”的问题也可以理解成，仿真往往是跟着specification走的，构建的场景往往也是围绕着spec，那么设计中可能植入的木马、多余的逻辑、影响安全的部分，这些对于更注重安全性的设计而言，static & formal也有能力可以探查。

在OneSpin被Simens收购以后，它的工具也就并入了Questa验证套件当中，这张图是讲他们围绕着static & formal还做了哪些新鲜的东西让人眼前一亮“beyond Questa Formal”。后面的一些内容也都是围绕着这张特性图来看的，有不少formal的应用让人觉得惊喜，一看就是研发团队跟着客户一起琢磨出来再细细打磨的好东西。

这张图意图在表明一个更为细致的流程，从requirement, plan, run再到analyze, monitor。在早期的话，如果有requirement trace的工具作为硬件软件需求库、再到测试计划的分析创建、再到回归测试的管理，这部分可以走在验证之前（持续交付CI的过程）。在持续交付也就是每周在测试实际时，可以让static & formal & simulation共同参与进来。这样至少在仿真能够跑完整场景前，static & formal就可以get answer earlier than simulation without testbench。这个CI过程也是这次研讨会带给客户的认知，只不过有的时候不是不愿意尝试，而是我们都知道formal的apps应用庞杂，每个分支都需要有学习曲线，而且还需要对足够的经验来让它有实际产出。

在同时投入静态、动态方法后，只要底层有统一的覆盖率数据格式，每周就可以基于此进行分析了。这个流程跟其它家EDA公司推出的consistent flow大差不差，看起来都是挺美好的，但一般只有采用了各家EDA公司的全家桶以后，这种flow才能顺利建立起来，而如果分别采用了不同的工具，那么中间的黏合部分，我认为regression工具就必须有高度的customization能力才能把不同工具的启动、报告、分析部分结合起来。

这里我得推一推我们合作伙伴Quickor开发套件的回归工具RunFab，V3课程的系统验证模块也有这个回归工具的介绍和使用，该工具适合将多个协同小组所开发的不同模块、子系统乃至系统的验证流程（Makefile/Perl/Python/Shell等脚本）按照模块化、继承方式轻松整合在一起，对于IC开发实际过程而言，更倾向于IC团队本身，不会与各家EDA工具有深度绑定的掣肘，应用方便，有兴趣的公司也可以跟我们取得联系，试用Quickor工具套件。

这张图对指导static & formal在何时介入验证过程有指导意义。可以看到在testbench ready之前，static & formal有很多app都可以投入应用，而且rtl designer就可以完成这些事情（lint/check register/cdc/rdc/check x/unreachable coverage analysis等），只有像property/check connect这些事情会更面向验证人员一点。说白了，designer可以同样做不少事情，而不是从项目上就把rtl design以外的事情都交给了verifier……

为了“秀肌肉”，OneSpin将一些开源设计作为输入，并使用不同的static & formal apps做了检查，然后从数据可以看到发现了多种类型的bug，包括功能对不上的（Spec）、边界情况（corner case）以及安全问题。

处理器的验证是一个单独的验证领域，需要对指令集、架构和功能描述均展开验证，而传统的仿真验证会面临很大压力，比如core作为一个“整体”，在验证它的流水线时传统仿真无法轻松撞出一些corner case，如果发生了指令执行错误，调试也会有难度（因为它不是简单的数据处理，而可能需要根据场景不同、调试方法也有不同），最后覆盖率的收敛到了后期也成了问题。

这次OneSpin研讨会上带来的第一个新鲜app就是协助RISC-V核验证的工具。它旨在让验证提速（尤其早期在没有UVM验证环境的时候）、并加速覆盖率的收敛。如果是以往的形式验证，那么往往需要这方面的专家/AE介入进来协助客户一同完成。而OneSpin这里的思路是降低“边际成本”，在标准指令集的基础上实现工具介入的自动化，比如不再需要单独定义覆盖率、自动提取微架构、生成断言等。

如何使用工具的PPT我没有拍到，不过大家可以想象就是一种类似填表的方式，告诉工具指令集、自定义指令、微架构、总线类型这些部分，接下来的事情就可以交给工具来完成。尽管可能实际工程中这部分setup要复杂一些，但自动化地完成处理器的检查、发现bug、每一项检查都可以自动生成断言、覆盖率还能在此基础上快速提升，这一切听起来还是很让人兴奋的。

接下来的FPU的formal app也是紧跟潮流的，在AI领域浮点运算单元是一个标准件，而FPU在实现时如果遵循IEEE-754标准的话，那么FPU App也可以帮助客户实现验证的自动化。

这种formal app的思路看起来就更像针对特定场景的“点”状应用，既解决了客户不知道怎么将formal带入到工作中，也尽可能让它们在特定的场景中“开箱即用”。这次研讨会上的App在我所了解的各家formal工具信息中，OneSpin是走到前面的。

Security验证的formal app，OneSpin不是第一家，但它在这方面的应用堪称是“打直拳”的典范。如果想要让工具检查出来A点到B点的path是否可能会存在数据泄露，只需要下面这种简单的配置即能够让工具帮助检查出是否可能有造成数据泄露的路径。而且大家可能会将这种模式跟formal经常用到的connection check做联想。毕竟两种情况面对大型的设计都可能会遇到空间爆炸的问题，而这次OneSpin竟然说他们已经有方法可以解决这种大设计的问题，而且还不用为此设置blackbox。什么？！这也听着很有趣好吗！