【忆芯技术分享】设计验证中的“黑魔法”——形式验证

近年来，数字芯片的设计越发复杂，设计验证的工作量也越来越大，各种自动化脚本和工具逐渐被工程师们运用了起来。形式验证（formal verification）作为一种高效、全面的验证方法逐渐被业内重视，并被用作动态测试的替代方式。形式验证能够在不创建仿真平台和测试向量的前提下，利用数学算法，并以类似于穷举的方式实现设计行为空间的全覆盖，可大幅缩短验证周期，并能轻松的找到边界条件下的隐藏漏洞。

设计验证可分为动态验证和静态验证两种形式。动态验证需要验证工程师编写测试平台，给DUT手动灌入受约束的随机激励。从2000-2004年推出的eRM和RVM，到数年后的OVM、VMM和UVM，都属于动态验证方法。静态验证可分为等价性检查（equivalence checking）和属性检查（property checking），前者将RTL和网表、修改后的RTL、C/C++模型进行对比检查，后者则需要使用PSL/SVA语言来编写property，formal工具会尝试证明这些assert property，或者找出它们的反例。此文描述的形式验证，均指FPV（formal property verification）。

图1 设计验证的分类

一►

Formal相对simulation所具有的优势

形式验证和动态验证的验证思想和方法有着显著不同，依赖于验证平台的传统动态验证具有以下相对不足：

① 开发一个复用性好的通用性测试平台占用的时间和精力很多。

② 通常testbench在开发过程中会产生比RTL更多的漏洞，环境的debug会占用更多精力。

③ 测试用例编写不合理可能造成假pass而被忽略。

④ 测试用例往往难以覆盖全所有的边界情况。

在使用formal验证替代simulation时，验证流程可大为缩减，如下图所示：

图2 formal和simulation的验证流程对比

（来源How formal verification saves time in digital IP design - EDN）

可见，formal相对simulation验证，完全不需要进行验证平台和测试用例的构建，可以节省大量时间。

假设将DUT的各个可能的状态以点的形式表现出来，则在每个仿真cycle时，simulation和formal对DUT的状态覆盖情况如下图所示。

图3 simulation和formal对DUT状态的覆盖情况

Simulation的随机化测试用例，将是一条串起各个圆点的固定折线。如果需要打到更多的设计漏洞，则需要更多的测试用例，并对难以覆盖的边界情况编写定向用例。而formal工具会以类似于穷举的方法，遍历每个仿真时刻下所有的可能状态跳转，能够快速且全面的找到隐藏的bug。

二►

Formal验证的劣势与局限

formal相对于simulation最大的劣势在于行为描述方式，sv作为一种仿真语言不需要经过综合，因此可以使用class，queue等结构化的语法，描述一种行为时更方便。做好formal验证最重要的就是掌握好各种断言语法，但断言语法并不像SV那么方便，利用有限的断言规则去描述复杂的场景，本身也是一个不小的挑战。另外，formal验证需要语法可综合，因此在描述DUT行为时候更困难。

formal工具在所有可能空间内去正确DUT行为正确，其计算量也是超过仿真的，通常DUT规模要求小规模或中等规模，并且pipeline不能太长，否则极易不收敛。

图4 复杂度与计算所需时间的关系

想要覆盖更复杂的情况，只需要增加测试用例，所需时间是线性增长的，而formal计算所需时间则成指数增长。因此每个assertion尽量不要太长，针对一个复杂的设计行为流程，则可将其进行拆分。

针对上述formal的优缺点，结合EDA公司推出的多种形式化流程工具（如dead code analysis和formal property check等），一个复杂设计的UVM验证流程，可以由图2转换成下图所示的新流程。

图5 新的验证流程

（来源How formal verification saves time in digital IP design - EDN）

可以将一个复杂设计中适合formal验证的部分剥离出来，利用EDA公司推出的多种formal工具，先单独对其进行充分的formal验证，其后就可认为它是一个golden模块，再对整体设计进行UVM验证。

三►

四步快速创建Formal环境

Formal验证环境不同于基于UVM的功能验证环境，不需要额外的太多东西，有了DUT之后，只需以下几个文件即可开始工作：启动脚本文件（如Makefile等）、SVA文件、top文件、initial文件。

当拿到设计代码之后，可以由以下四个步骤快速开始formal验证：

① 首先创建一个top文件将DUT例化在其中，并对其中必要的port进行连接。

② 编写SVA文件，新建一个sva module，直接将对应DUT的所有port复制过来，并将所有output改为input。可以先在其中写一条简单的assertion property，并在module外将其与DUT进行bind。

③ 编写initial文件，在此文件中用formal工具支持的tcl命令，来设置初始条件，如复位、时钟频率、时钟域设置、常数配置等操作。

④ 编写启动脚本文件，包含formal工具支持的编译、运行、调试、清除命令等。

在特定formal工具的user guidance作为参考下，以上步骤都能快速完成。至此，一个formal环境就可以跑起来了。

Simulation和formal的验证环境对比图如下所示，formal不需要创建复杂的环境组件，只需创建一个包含各种property的SVA module，其它的都可以交给工具。

图6 formal环境和simulation环境对比

对于部分没有在initial文件中配置的DUT输入端口，formal工具将自动给他们随机值。某些不合理的随机，会造成某些assertion fail。对于这种情况，一般可采用三种方法：initial文件配置、top文件配置、assumption约束。

SVA文件中的property可以assume标志为assumption，则formal工具会强制满足此property。也可以assert标志位assertion，则工具会在每个时钟检查其是否成立。

一个简单的例子，一个名叫test的module，其有一个input信号为A，一个output为B，则可以以下图方式将输入A约束为0到15之间的固定值，并在每个时钟去检查它是否满足约束。

图7 一个简单的示例

一般情况而言，不建议验证一开始就添加大量的assumption，往往在工具找出某个assertion的反例，经过debug后发现需要添加某个约束，再来添加此合法的assumption。

四►

实际应用场景

目前，忆芯高端企业级主控STAR2000的芯片即将量产。在其设计验证阶段，P channel模块利用formal的方法，轻松的覆盖到了一个simulation难以构造的边界场景。同时Q channel模块在一个复杂设计中已经整体验证通过，但利用formal验证的方法仍然发现了一个隐秘的bug，这些情况利用传统动态仿真则难以发现。

借助EDA厂商提供的公共SVA/PSL断言库，除了验证师外，设计师也可以将形式语言预置到设计中去，进一步确保一些中要功能和时序的正确性。此外设计也可以采用对SVA语言友好的设计风格，共同推动和实现可验化设计的理念。

忆芯科技

核心职位火热招聘中

扫描二维码了解更多信息

END

推荐阅读

9-20

9-14

忆芯科技

北京忆芯科技有限公司成立于2015年底，作为国内较早从事高性能固态硬盘主控芯片研发的企业，致力于成为赋能大数据应用的芯片全球领导者。经过7年的发展，公司已成长为国内领先的高端PCIe SSD主控芯片和成品盘供应商，为各行业的信息化发展提供高质量芯片级底层保障，业务方向覆盖消费级、工业级和企业级，主控芯片及解决方案。

忆芯科技核心成员具有多年研发经验和多项研发成果，拥有从底层算法到芯片设计，再到解决方案设计等多方面的丰富经验。在坚持自主研发基础上，研发的芯片产品拥有260余项自主知识产权，并创新性地将处理器架构首次引入存储领域；现已成功完成4款高端消费级、企业级SSD主控芯片流片，所研发的高性能低功耗NVMe SSD主控已量产出货。公司总部位于北京，在上海、成都、合肥、厦门、深圳分别设有研发中心和客户技术支持中心。