形式化验证是一种验证方法，而实际应用方向主要有两方面，一是综合前后的等价性检查，二是RTL设计的功能验证。
本文所讲的是形式化验证方法在RTL设计功能验证方向的应用。
芯片验证的两个方法，一个是模拟仿真验证，另一个是形式化验证。
模拟仿真验证是目前最主流的验证方法，主要是以 UVM 为代表的验证方法学，特点就是搭建模拟仿真环境，通过随机化激励进行模拟仿真，reference module作为验证标准进行结果数据的check，以收集覆盖率的方式作为验证进度的参考，当代码覆盖率和功能点覆盖率达到100%时，做到sign off。
由此看来，模拟仿真的优点就是基本不受设计复杂度的影响，而缺点就是验证环境搭建较复杂，测试激励手动添加，收集覆盖率周期较长，尤其是Corner场景的覆盖很让人头疼。
形式化验证从某层面看似乎让人省心。形式化方法简单的说就是用数学工具进行定义、开发和验证，它会对设计电路进行数学建模，然后穷举系统运行过程中电路所能达到的所有状态，以断言的形式完成设计电路的功能验证和规则检查（也可以通过reference model的形式，做结果数据的check）。
听起来似乎完美，但是这要依赖强大的运算系统和EDA工具，否则会发生状态爆炸问题，长时间无法得出证明结果。以目前的形式化验证工具来看，还不足以吃进一个超复杂的设计电路，来完全替代模拟仿真的验证方法。
所以，在芯片的验证中，随机仿真验证和形式化验证往往是相辅相成，一个更适合系统级功能验证，一个更适合模块级的功能验证。除此之外，还有FPGA的硬件加速测试，这三种验证手段可谓是三位一体，相辅相成。
个人认为，形式化验证是基于严格的数学算法和模型，根据设计功能提取电路规则的属性描述，并穷举系统运行过程中电路所能达到的所有状态，自动进行数学分析和证明。验证过程如下：
以上的形式化验证过程就像做一道数学证明题，用数学方法证明该命题是否成立，而这个证明过程是验证工具完成的，工程师不需要关心。
目前，业界主流的形式化验证工具主要有Cadence的 JasperGold 和 Synposys 的 VC-Formal。
形式化验证使用的是 SVA (SystemVerilog Assertion) 语言，属于SV的一部分，下面对SVA基本的使用语法进行说明。
SVA的语法主要分为三种使用类型：assume、assert、cover。
使用的基本规则为，先描述一个property，然后为property设置为assume或assert或cover，命名时习惯性将property名字添加“P_”前缀，将assume名字添加“ASM_”前缀，将assert名字添加“AST_”前缀，将cover名字添加“COV_”前缀。注：建议所有属性带时钟沿触发条件。
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语法的使用做简单介绍：
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语法的使用做简单介绍：
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，其常用的使用方法有两种类型，
这里只对FPV进行介绍，也就是 Formal Property Verifycation。
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
analyze -v2k –f $DES_PATH/design.flist
analyze –sva –f $PRO_PATH/property.flist
elaborate –top top_module_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”
启动验证环境很简单，验证流程主要依靠启动脚本的设置，而验证环境的启动只需在终端敲下启动命令即可，如下：
jg FPV_project_name.tcl
当然不是！
换句话说，形式化验证不能验证完全，虽然不能做到sign off，但是可以将前期暴露的语法bug和设计bug进行修复，最终验证不完全，无非表明我不一定是对的，但也没找到我的错误，说明设计代码已经达到一定成熟度。
复杂的设计验证时间通常较长，不容易完成验证，但是，依据设计的特性，也是可以通过一些手段完成验证，下面以典型设计举例。
此设计有以下几个特点：
以上方法还未在实际工程中使用过，待后续总结
