欢迎光临专业集成电路测试网~~欢迎加入IC测试QQ群:111938408

专业IC测试网

当前位置: 网站主页 > 相关技术 > 芯片制造 >

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

时间:2024-05-29 20:28来源:TrustZone 作者:ictest8_edit 点击:


前言


形式化验证是一种验证方法,而实际应用方向主要有两方面,一是综合前后的等价性检查,二是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或其他存储类模块,设计本身主要验证的是控制逻辑,从而可以减少存储单元来针对设计完成抽象模型,可以有效的减少状态空间。
· 黑盒化:将不关心的设计设置黑盒,可以有效的减少状态空间
· 断点:待了解
以上方法还未在实际工程中使用过,待后续总结
 
顶一下
(0)
0%
踩一下
(0)
0%
------分隔线----------------------------
发表评论
请自觉遵守互联网相关的政策法规,严禁发布色情、暴力、反动的言论。
评价:
用户名: 验证码: 点击我更换图片