Formal验证技术总结

本文

主要介绍本人使用形式化验证的一些经验总结。

版本 说明
0.1 初版发布
0.2 添加JasperGold的tcl脚本启动环境

背景

  • 验证工具: Cadence 公司的 JasperGold

写在前头

形式化验证是一种验证方法,而实际应用方向主要有两方面,一是综合前后的等价性检查,二是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语法的使用做简单介绍:

  • 标准写法
1
2
3
4
property P_property_name;
    @(posedge clk) (condition==1'b1) -> (result==1'b1);
endproperty
ASM_property_name: assume property (P_property_name);
  • 精简写法
1
ASM_property_name: assume property (@(posedge clk) (condition==1'b1) -> (result==1'b1));

Assert

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

  • 标准写法
1
2
3
4
property P_property_name;
    @(posedge clk) (condition==1'b1) -> (result==1'b1);
endproperty
AST_property_name: assert property (P_property_name);
  • 精简写法
1
AST_property_name: assert property (@(posedge clk) (condition==1'b1) -> (result==1'b1));

Cover

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

  • 标准写法
1
2
3
4
property P_property_name;
          @(posedge clk) (condition==1'b1) -> (result==1'b1);
endproperty
COV_property_name: cover property (P_property_name);
  • 精简写法
1
COV_property_name: cov property (@(posedge clk) (condition==1'b1) -> (result==1'b1));

JasperGold的使用

本文使用的形式化验证工具是JasperGold,其常用的使用方法有两种类型,一个是SEC,对模块功能做对等性检查,另一个是FPV,基于规则特性的功能验证。这里只对FPV进行介绍,也就是 Formal Property Verifycation。

验证环境

  1. FPV_project_name:整个FPV的验证环境。
  2. Report:用来存放验证报告。
  3. Source:整个FPV环境的文件源。
  4. FPV_project_name.tcl:FPV验证环境的启动脚本。
  5. Design:文件源中的设计文件,也可以不存放设计文件,而由design.flist指定设计文件。
  6. Property:文件源中的验证文件(SVA),提取设计文件的属性。
  7. Refer_model:此文件为参考模型文件,根据需求创建,非必须。

启动脚本

  • 设置环境变量
1
2
3
set FPV_ROOT    /FPV_project_path
set DES_PATH    $FPV_ROOT/source/design
set PRO_PATH    $FPV_ROOT/source/property
  • 设置功能点收集选项
1
2
set_capture_elaborated_design on
check_cov init exclude_bind_hierarchies enable_prove_based_proff_core
  • 编译设计文件 (注:v2k指IEEE 2001 标准)
1
analyze -v2k f $DES_PATH/design.flist
  • 编译验证文件
1
analyze sva f $PRO_PATH/property.flist
  • 设置顶层
1
elaborate top top_module_name
  • 设置时钟和复位 (注:如果复位是低位有效,则为 ~reset_signal_name)
1
2
clock clock_signal_name
reset reset_signal_name
  • 设置最长验证时间
1
set_prove_time_limit 24h
  • 启动验证
1
prove -all
  • 生成报告
1
report summary force result file report/FPV_project_name.rpt
  • 其他

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

启动命令

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

1
jg FPV_project_name.tcl

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

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

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

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

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

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

当然不是!

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

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

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

  1. 完成设计不加任何特性检查,直接启动形式化验证工具,可将暴露的语法错误和警告修复,提高设计代码质量。当然反过来,验证人员可先启动形式化验证工具,将暴露的语法错误和警告提单给设计人员。
  2. 设计时对于显而易见的规则特性边设计边记录,待设计交付验证人员时,可先启动形式化验证,修复前期bug,提高设计代码质量。
  3. 模拟仿真中收集覆盖率,对于较难收到的功能点可利用形式化验证工具去设置cover,辅助模拟仿真创建定向用例。这里提两点,一是需要确定输入的场景作为输入约束,二是无需保证形式化验证的正确性,因为只是提取测试激励,正确性由模拟仿真保证。

复杂设计如何完成验证

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

设计结构

此设计有以下几个特点:

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

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

  1. 依据功能类型,分类验证,各个功能依次验证。
  2. 约束输入,单功能验证仅提交一次,运算数据由工具遍历,验证功能正确性。
  3. 除流水线控制寄存器之外,其他寄存器不加复位,工具会将其初始值进行遍历,可等效为激励输入前模块的任何状态。
  4. 凡是影响流水线行进的输入,全部添加约束,可以约束停顿周期为1~2,或直接约束为无停顿,暂不验证流水线控制功能。
  5. 数据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。
  6. 对流水线控制功能的验证,在其算法功能验证的正确基础上,将数据进行适当约束,减少遍历空间,主要验证流水线控制功能。
  7. 其他手段有待后续补充。

其他减少状态空间的方法

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

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

推荐书籍

  • 《SystemVerilog Assertion应用指南》
  • 《Formal Verification: An ESSential Toolkit For Modern VLSI Design》
  • JasperGold使用手册(需要该资料可私下联系)

文章原创,可能存在部分错误,欢迎指正,联系邮箱 cao_arvin@163.com。