芯片验证 | Formal验证技术总结

前言

形式化验证是一种验证方法，而实际应用方向主要有两方面，一是综合前后的等价性检查，二是RTL设计的功能验证。

本文所讲的是形式化验证方法在RTL设计功能验证方向的应用。

模拟仿真验证和形式化验证

芯片验证的两个方法，一个是模拟仿真验证，另一个是形式化验证。

模拟仿真验证是目前最主流的验证方法，主要是以 UVM 为代表的验证方法学，特点就是搭建模拟仿真环境，通过随机化激励进行模拟仿真，reference module作为验证标准进行结果数据的check，以收集覆盖率的方式作为验证进度的参考，当代码覆盖率和功能点覆盖率达到100%时，做到sign off。

由此看来，模拟仿真的优点就是基本不受设计复杂度的影响，而缺点就是验证环境搭建较复杂，测试激励手动添加，收集覆盖率周期较长，尤其是Corner场景的覆盖很让人头疼。

形式化验证从某层面看似乎让人省心。形式化方法简单的说就是用数学工具进行定义、开发和验证，它会对设计电路进行数学建模，然后穷举系统运行过程中电路所能达到的所有状态，以断言的形式完成设计电路的功能验证和规则检查（也可以通过reference model的形式，做结果数据的check）。

听起来似乎完美，但是这要依赖强大的运算系统和EDA工具，否则会发生状态爆炸问题，长时间无法得出证明结果。以目前的形式化验证工具来看，还不足以吃进一个超复杂的设计电路，来完全替代模拟仿真的验证方法。

所以，在芯片的验证中，随机仿真验证和形式化验证往往是相辅相成，一个更适合系统级功能验证，一个更适合模块级的功能验证。除此之外，还有FPGA的硬件加速测试，这三种验证手段可谓是三位一体，相辅相成。

什么是形式化验证

个人认为，形式化验证是基于严格的数学算法和模型，根据设计功能提取电路规则的属性描述，并穷举系统运行过程中电路所能达到的所有状态，自动进行数学分析和证明。验证过程如下：

以上的形式化验证过程就像做一道数学证明题，用数学方法证明该命题是否成立，而这个证明过程是验证工具完成的，工程师不需要关心。

目前，业界主流的形式化验证工具主要有Cadence的 JasperGold 和 Synposys 的 VC-Formal。

SVA语法

形式化验证使用的是 SVA (SystemVerilog Assertion) 语言，属于SV的一部分，下面对SVA基本的使用语法进行说明。

SVA的语法主要分为三种使用类型：assume、assert、cover。

使用的基本规则为，先描述一个property，然后为property设置为assume或assert或cover，命名时习惯性将property名字添加“P_”前缀，将assume名字添加“ASM_”前缀，将assert名字添加“AST_”前缀，将cover名字添加“COV_”前缀。注：建议所有属性带时钟沿触发条件。

Assume

Assum即假定之意，也就是假定某些信号符合某规则特性，最常见的就是给输入信号添加约束，下面对assume语法的使用做简单介绍：

property P_property_name;
    @(posedge clk) (condition==1'b1) -> (result==1'b1);
endproperty
ASM_property_name: assume property (P_property_name);

• 精简写法

ASM_property_name: assume property (@(posedge clk) (condition==1'b1) -> (result==1'b1));

Assert

Assert即断言之意，也就是认为某些信号符合某规则特性，出现反例则报错，最常见的就是给关键信号依据特定属性设置断言，来进行特性检查，下面对assert语法的使用做简单介绍：

property P_property_name;
    @(posedge clk) (condition==1'b1) -> (result==1'b1);
endproperty
AST_property_name: assert property (P_property_name);

• 精简写法

AST_property_name: assert property (@(posedge clk) (condition==1'b1) -> (result==1'b1));

Cover

cover即覆盖之意，也就是对某些信号的某规则特性进行采样，反馈是否覆盖该特性，下面对cover语法的使用做简单介绍：

property P_property_name;
          @(posedge clk) (condition==1'b1) -> (result==1'b1);
endproperty
COV_property_name: cover property (P_property_name);

• 精简写法

COV_property_name: cov property (@(posedge clk) (condition==1'b1) -> (result==1'b1));

JasperGold的使用

本文使用的形式化验证工具是JasperGold，其常用的使用方法有两种类型，

• 一个是SEC，对模块功能做对等性检查，
• 另一个是FPV，基于规则特性的功能验证。

这里只对FPV进行介绍，也就是 Formal Property Verifycation。

验证环境

• FPV_project_name：整个FPV的验证环境。
• Report：用来存放验证报告。
• Source：整个FPV环境的文件源。
• FPV_project_name.tcl：FPV验证环境的启动脚本。
• Design：文件源中的设计文件，也可以不存放设计文件，而由design.flist指定设计文件。
• Property：文件源中的验证文件（SVA），提取设计文件的属性。
• Refer_model：此文件为参考模型文件，根据需求创建，非必须。

启动脚本

• 设置环境变量

set FPV_ROOT    /FPV_project_path
set DES_PATH    $FPV_ROOT/source/design
set PRO_PATH    $FPV_ROOT/source/property

• 设置功能点收集选项

set_capture_elaborated_design on
check_cov –init –exclude_bind_hierarchies –enable_prove_based_proff_core

• 编译设计文件 (注：v2k指IEEE 2001 标准)

analyze -v2k –f $DES_PATH/design.flist

• 编译验证文件

analyze –sva –f $PRO_PATH/property.flist

• 设置顶层

elaborate –top top_module_name

• 设置时钟和复位 (注：如果复位是低位有效，则为 ~reset_signal_name)

clock clock_signal_name
reset reset_signal_name

• 设置最长验证时间

set_prove_time_limit 24h

• 启动验证

prove -all

• 生成报告

report –summary –force –result –file “report/FPV_project_name.rpt”

• 其他
  以上只说明了基本设置，其他详细设置可参考手册或JasperGold的Tcl Command Help。

启动命令

启动验证环境很简单，验证流程主要依靠启动脚本的设置，而验证环境的启动只需在终端敲下启动命令即可，如下：

jg FPV_project_name.tcl

关于形式化验证的个人总结

什么样的设计适合用形式化验证

• 规模较小：设计模块太大对应验证复杂度较高，导致验证时间过长。
• 功能独立：功能独立的设计更容易提取规则属性。
• 时序较短：时序较长会导致验证复杂度增大，验证时间指数增长。
• 接口清晰：接口清晰便于对输入添加约束，避免非法输入影响验证结果。

形式化验证中影响验证时间的因素

• 设计复杂度：设计复杂度高，肯定验证时间长，这也是为什么形式化验证不适合大的设计模块。
• 时序较长：形式化验证是所有状态的全遍历，时序每增加一个cycle，所增加的遍历空间并非只是此cycle，还包括此cycle与前几个cycle的状态组合，换句话说，时序增加，遍历空间指数增长。
• 设计中存在时序控制：比如advance_pipeline对pipeline进行使能控制的此类信号，以及所有影响流水线不能依次脉动流出的控制信号。
• 设置的特性检查：设置的特性检查越多越复杂，对应的验证时间越长，如果以reference model形式进行数据结果check，所需验证时间最长，但是若只提取设计特性又很难做到signoff标准。

形式化验证不能验证完全是不是就无任何作用

当然不是！

• 形式化验证工具进行了语法检查，可确定设计逻辑语法无误。
• 形式化验证工具进行了部分特性检查，可确定已验证的特性符合设计规则。

换句话说，形式化验证不能验证完全，虽然不能做到sign off，但是可以将前期暴露的语法bug和设计bug进行修复，最终验证不完全，无非表明我不一定是对的，但也没找到我的错误，说明设计代码已经达到一定成熟度。

形式化验证工具的其他用途

• 完成设计不加任何特性检查，直接启动形式化验证工具，可将暴露的语法错误和警告修复，提高设计代码质量。当然反过来，验证人员可先启动形式化验证工具，将暴露的语法错误和警告提单给设计人员。
• 设计时对于显而易见的规则特性边设计边记录，待设计交付验证人员时，可先启动形式化验证，修复前期bug，提高设计代码质量。
• 模拟仿真中收集覆盖率，对于较难收到的功能点可利用形式化验证工具去设置cover，辅助模拟仿真创建定向用例。这里提两点:

• 一是需要确定输入的场景作为输入约束，
• 二是无需保证形式化验证的正确性，因为只是提取测试激励，正确性由模拟仿真保证。

复杂设计如何完成验证

复杂的设计验证时间通常较长，不容易完成验证，但是，依据设计的特性，也是可以通过一些手段完成验证，下面以典型设计举例。

设计结构

此设计有以下几个特点：

• 设计中stage1输入，stage5输出，中间需寄存四拍。
• 设计中分为流水线控制信号、数据信号和控制信号、组合逻辑三个部分，流水线控制信号带复位。
• 设计中为单向流动，无bypass，也就是流水线前后独立，无反馈。
• 设计中带advance_pipeline，流水线的使能控制，也就是流水线可能锁定n拍后重新启动。
• 设计中模块支持多功能类型，也就是op_type。

复杂设计的形式化验证方案

• 依据功能类型，分类验证，各个功能依次验证。
• 约束输入，单功能验证仅提交一次，运算数据由工具遍历，验证功能正确性。
• 除流水线控制寄存器之外，其他寄存器不加复位，工具会将其初始值进行遍历，可等效为激励输入前模块的任何状态。
• 凡是影响流水线行进的输入，全部添加约束，可以约束停顿周期为1~2，或直接约束为无停顿，暂不验证流水线控制功能。
• 数据check语法采用单比特，如“data_a[3:0]==data_b[3:0]”改为“data_a[3]==data_b[3], data_a[2]==data_b[2] ……”，前者遍历空间是2^4，后者遍历空间2*4。
• 对流水线控制功能的验证，在其算法功能验证的正确基础上，将数据进行适当约束，减少遍历空间，主要验证流水线控制功能。
• 其他手段有待后续补充。

其他减少状态空间的方法

• 抽象模型：如fifo或其他存储类模块，设计本身主要验证的是控制逻辑，从而可以减少存储单元来针对设计完成抽象模型，可以有效的减少状态空间。
• 黑盒化：将不关心的设计设置黑盒，可以有效的减少状态空间
• 断点：待了解

以上方法还未在实际工程中使用过，待后续总结

推荐书籍

• 《SystemVerilog Assertion应用指南》
• 《Formal Verification: An ESSential Toolkit For Modern VLSI Design》
• 《JasperGold使用手册》

原文链接：https://www.wenhui.space/docs/07-ic-verify/formal/formal/