保序模块的formal fpv 验证

赵亚雪，植 玉，梁其锋，石义军

(深圳市中兴微电子技术有限公司，广东 深圳 518054)

0 引言

芯片验证方向经过多年的探索和积累已经有一套较为完备的验证体系[1]。其中，simulation 验证和formal 验证是两大常用的验证方法。从对测试点的覆盖程度上来说，两者的区别在于simulation 着眼于测试空间中的单个点，而formal 验证可以完全覆盖输入空间，从而能在约束条件下有效证明设计的准确度[2]，formal 验证方法能在短时间内遍历所有可能的激励，从而大大提高验证效率[3]，因此近年来formal 验证方法得到了越来越多的关注。

formal 验证工具大体可以分为两类[4]，一类是MFV(Mainstream Formal Verification)，其具有成熟的功能，能实现高度自动化验证。另一类是FPV(Formal Property Verification)，需要手动开发验证环境，编写property[5]。对于逻辑较为复杂、难以调用工具自带模型的模块更倾向于选择FPV 工具来进行验证。

保序模块用于确保处理器内部读、写访问严格按照既定的顺序处理，其与时序控制以及流水线控制密切相关，设计规模较大，逻辑复杂度较高，采用formal fpv 工具，本文按照验证对象介绍、Design Review、验证环境搭建、验证模型编写、JasperGold debug 的流程来展开介绍。

1 验证对象简介

保序模块是我司某存储器系统中用于保证读、写访问顺序的模块，基本框图如图1 所示，主要包括B 指令译码、B 数据写访问缓存、B 数据保序、B 数据提前返回、A 数据保序、A 数据提前返回、重读等功能。

图1 保序模块基本框图

保序模块会对输入的B 指令进行译码，译码后的B数据写访问会经过28 级流水buffer 缓存，在流水线上会对B 数据写请求地址相关的访问进行保序处理，同时会判断B 数据读与B 数据写是否提前返回，以及重读指示信号是否产生。对于A 数据访问来说，A 数据写访问也会经过28 级流水buffer 缓存，在流水线上会对A 数据访问进行保序处理，也会判断A 数据写数据是否提前返回。

其中，地址相关的保序需满足：读写同拍发生，认为读操作期望读取旧值；先写后读场景，认为读操作期望读取写入后的新值。

2 Design Review

常用的formal sign-off flow 可以分为两种情况。

一种是传统formal sign-off flow，如图2 所示，特点是所有的断言都需要被证明。对于这种sign-off flow，理想的RTL 代码行数应在1 500～3 000 范围内。在传统Formal sign-off flow 中工具根据手动编写的断言自动提取生成coverage，不需要再编写cover，保序模块验证正是采用这种传统的方法。

图2 传统formal sign-off flow

另一种是新型formal sign-off flow，如图3 所示，特点是允许有证不出来的断言，也就是说允许有处于undetermined 的断言，对于证不出来的断言需要手动编写function cover，对这种sign-off flow 来说，理想的RTL 代码行数应在3 000～5 000 范围内。

图3 新型formal sign-off flow

通过Design Review 可以梳理出fpv 验证的大框架。保序模块涉及流水数较多有29 级，且前级流水的信号会对后级流水信号的变化产生影响，从input-output 信号通路角度来考虑，将保序模块拆分成6 条通路，分别对每条通路使用formal fpv 进行验证。

3 验证环境搭建

保序模块验证平台由三部分组成，分别是rtl_dmss、signoff、sva，其中rtl_dmss 用来存放设计RTL 代码，signoff用来存放filelist、tcl 脚本以及编译仿真过程中产生的临时文件，sva 用来存放验证模型、验证平台的环境文件。

在验证平台环境中首先定义了模块端口上的所有信号，然后将待测设计DUV 与验证模型连接起来作为激励入口，验证平台结构如图4 所示。

图4 验证平台结构

在没有外部约束的情况下，formal 会穷举整个输入空间，所以为了避免出现不符合设计需求的场景，需要在验证模型中添加相应的约束。验证输出和待测设计输出的比对工作则放到了验证模型的assertion 部分，在assertion 部分会进行一致性比对和时序检查。

4 验证模型编写

由于保序模块涉及29 级流水且逻辑较为复杂，fpv工具自带的模型并不适合保序模块，需要手动搭建各条通路的验证模型。保序模块的验证模型包括模块功能模型、激励约束和断言三部分。

4.1 功能模型编写

功能模型用来模拟被测对象的功能，通过将功能模型的输出结果与待测对象的输出进行比对、检查，可以得知待测对象功能的正确性。功能模型使用Verilog 语言来编写而不是SystemVerilog，这是因为功能模型一定要可综合，而SystemVerilog 有些语法不可综合。对于保序模块来说，功能模型以cycle 为单位进行建模，描述了模块处于29 级流水的工作情况。

4.2 激励约束编写

simulation 方法通过接口平台产生transaction，再把transaction 传输给参考模型和待测设计，而formal 验证方法会对约束后的激励进行遍历，也就是说formal 验证平台的激励来自约束条件，如图5 所示，激励约束可以分为legal 和illegal 两种。

图5 输入激励约束

工具会对所有输入信号进行全随机遍历，通过编写激励约束能保证输入信号满足待测设计的需求，而不会出现超出设计需求的场景。

值得注意的是，在编写激励约束时不要过约束，否则验证的完整性就会大打折扣。对于保序模块来说，调试初期可能存在过约束的场景，调试过程中再逐渐放开约束，保证验证的完整性和正确性。为了避免造成混乱，建议添加注释将过约束和正常约束加以区别，同时出于规范化考虑，可以给激励约束的名称添加“ASM_”前缀。

对保序模块的配置地址进行约束时，虽然配置地址可以是随机的，但在一次仿真中各个cycle 的配置地址需要保持不变，所以也需要对配置地址加以约束。

4.3 断言编写

为了检查待测设计的准确性，需要把功能模型输出与待测设计输出进行比较，通过断言来检查两者是否匹配。断言检查流程如图6 所示，当断言的所有状态都被分析证实后该条断言判断为proved。

图6 断言检查流程

formal fpv 断言编写的原则之一是简单化。对于bit位较多的信号可以按一定的规则对信号进行拆分，例如在保序模块中检查输出读地址的正确性，由于读地址信号有32×8 bit，包含8 个通道每个通道32 bit 地址，可以使用循环把读地址拆分成8 份，编写断言来检查每一份读地址的正确性。

出于规范化考虑，可以给断言的名称添加“AST_”前缀。为了避免断言调试出错，在复位信号有效时需要disable掉该断言，在保序模块中写作“disable iff(！core_sync_rst_n)”。

完备性是保序模块验证的重要衡量指标之一，通过给每条断言添加注释能方便地找出该条断言对应设计的哪些功能点，便于了解设计各个功能点是否都有断言覆盖。

5 JasperGold debug

5.1 JasperGold 工具介绍

运行tcl 脚本启动JasperGold 软件的UI 界面，可以看到各条断言的仿真结果，如图7 所示。

图7 断言仿真结果

JasperGold 的配置、编译和仿真都是通过tcl 命令来实现的，可以查阅相关命令的使用说明，如图8 所示。

图8 JasperGold 命令集

各条断言仿真结果可能有prove、unreachable、undetermined 三种情况。图7 中assert 前打绿勾表示断言验证通过，打叉表示该断言出现反例，可以双击查看波形进一步分析。打勾和感叹号表示断言的前提条件无法满足，需要检查约束条件是否过约束，debug 分析是验证模型问题还是待测设计问题。

当断言出现反例时，双击失败的断言可以打开对应的波形，波形能精准定位到出现反例的时刻，如图9 所示，深灰表示触发断言，浅灰色表示断言违例。

图9 反例断言仿真波形

5.2 debug 结果分析

在验证保序模块验过程中发现了一些设计的缺陷，对这些缺陷加以整理汇总，主要有以下几类。

第一类缺陷是待测设计中某些信号定义错误，这类属于比较直观的缺陷。在断言检查时发现验证输出的B数据读地址与待测设计输出的B 数据读地址不一致。定位问题发现是设计信号出现了位宽越界，养成良好的编码习惯能大大减少这种情况的出现。

第二类缺陷是待测设计某些通道的信号处理出错。保序模块读访问包含8 个通道，断言检查时发现输出的地址有效指示信号出错。通过前向追溯问题发现待测设计某一通道的位宽处理出错，该缺陷在更上一层次的系统验证中没有检查出来。这就要求在编写断言时，当遇到复杂的信号时可以将其拆分成多组，分别检查每组信号的时序，能迅速、精准地定位问题从而提高验证效率。

第三类缺陷是待测设计中循环处理出错。保序模块内信号的处理均受流水线控制，采用循环方法模拟流水线处理，在此过程中一些信号的赋值出错。通过断言检查发现验证输出与待测设计输出不一致，定位到写访问使能信号计算出错，进一步向前推算发现问题的源头是循环处理出错。对于这种问题链路过长的情况，如果从输出信号开始定位验证难度较大，可以通过添加辅助逻辑来缩短问题链路，从而降低问题难度。

6 结论

基于formal fpv 的验证方法在保序模块验证中有着很不错的效果，验证共发现8 单故障，其中一单故障发现了系统级验证遗漏的问题。formal fpv 验证能实现输入激励的全范围遍历，这给验证工作提供了极大的便利。但是，formal fpv 验证很大程度上依赖于断言编写的质量，且复杂的模块需要手动编写验证功能模型。

综合来看，对于设计相对简单的模块采用formal fpv验证能提高验证效率，加快验证收敛速度。