形式验证简介

通过纯数学方法分析两个网表的逻辑是否完全等价
一种静态比较，会遍历所有的组合保证逻辑等价性，不需要动态激励
比仿真可靠性高！！！仿真覆盖率低，且后仿非常慢。

常用工具：

Synopsys: Formality
Candence: LEC

形式验证在设计流程中的位置：

1、在综合后：保证综合过程没有出错，逻辑正确
2、后端布局布线后：使用综合网表和和布局布线后网表进行比较（上图位置不正确，不用再STA后）

形式验证的应用

1、综合的网表与RTL对比做形式验证。保证综合过程没有逻辑错误。保证综合后的网表是想要的。

2、后端网表与综合后的网表对比做形式验证。保证后端没有引入逻辑错误。（后端做完就可以做形式验证，不一定要等到静态时序分析做完）

3、做ECO的时候，ECO后的网表与ECO后的RTL做形式验证。（ECO当芯片已经流片出去了，工厂只做了一个底层，但金属层还没做可以做metalECO，发现某些容易修的bug后可以利用一些冗余的cell改变某些连线来修掉这个Bug，修改后端网表的同时对RTL也进行相应修改，然后将这两个文件进行LEC比较）

LEC所需要的文件

需要比对的两个文件，一个是标准的golden,一个是待比对的revised。
各种库文件的verilog model
约束文件：black box （IP）和pin constraint等
所用的工具——LEC（或者Formality）

LEC输出的文件

比较的结果报告
保留结果的session文件

形式验证LEC的流程以及分步骤讲解

流程

setup mode:
建立基本环境
读入设计
设置参数
LEC mode
映射golden以及revised所有比较点
比较设计
检查结果

所有的命令都有使用mode的限制

LEC比较流程

关键是所有的mapping point要一一对应映射
Mapping point主要有：
输入输出primary inputs/primary outputs
DFF
Latch
Black box
Tie-z cell
Cut point
（后面两种比较少碰到，中间任何的组合逻辑都不是mapping point,只会比较输出和触发器）cut point是手动设置的两个点）
示例：

比如3个触发器，经过一个组合逻辑驱动下一个触发器；首先LEC会确认RTL和网表中是否都又存在这些寄存器，然后3个触发器的输入有8种可能，最后再RTL和网表种遍历这些结果，看是否对应。

如何寻求帮助

man lec-command -v
help lec_command
LEC reference file/user guide

LEC命令行的两种模式

vpxmode:默认启动模式。运行效率较高。命令不同部分之间是空格。如：read library …大小写不敏感用空格隔开。
Tclmode:传统模式。命令由不同部分直接由下划线连接。例如：read_library…（用的较少）
Tclmode大小写敏感。

1、设置LEC环境

设置环境变量，如顶层的名字
创建目录结构，RPT等文件夹
设置一些自定义命令等
add alias new_name original_command

2、读取库文件

读取所有相关标准单元库的verilog model文件
使用read library 命令读取verilog model。如果有多个verilog model需要一次性读入。
例如：read library -both -verilog std_model.v std_mode2.v

3、读取设计文件

LEC把两个网表分别称为golden和revised。一般以RTL的作为golden。
read design -systemverilog -golden -sensitive（是不是大小写敏感） -root $working_design -file flist_rtl.f
read design -systemverilog -revised -sensitive -root $working_design -file syn.v

4、设置约束文件

主要是对特定的一些pin给予约束，如RST设置成无效值，scan mode设置成无效值等，scan mode=0代表是功能模式。
设置比较的参数，比较的方法。如按照名字映射还是按照功能映射。默认第一顺序都是按照名字映射。
可以手动设置下mapping point

5、LEC compare

进入LEC mode （set system mode LEC）
再次对没有map上的点做映射，并比较golden和revised中所有的mapping point

6、检查LEC结果

检查是否有没有mapping的点****一般有两种情况会导致unmap

extra unmap:只在其中一个design里有
Unreachable: 定义了reg但是没用到，这些point与PO直接没有路径

RTL中的mapping point与NET中的 mapping point一样多，且一一映射。（理想情况）

实际RTL多一些，多余的往往是RTL冗余的点造成的，这种情况是extra unmap。代码冗余不会有实际的问题。冗余的代码没有通路输出到PO就是unreachable。

检查所有mapping的点是否都是逻辑等价的

Equivalent
Inverted-equivalent（反相等价）
Sequential-merge（写了两段代码功能上比较接近，工具就会把这两段代码融合到一起，比如第一段代码有20个触发器，有5个是冗余的，最后会把它合并成15个，以减小面积）
Non-Equivalent
Abort （工具比较不出来）

前面三个都是表示相等
相反相位相等，最后到了端口上还是一一对应的。designer关心的应该是端口的输出结果。前面四个碰到的比较多，最后的比较少。

report mapped points
report unmapped points
report compare data
report black box
图形化界面可以打开电路，更有利于Debug

7、保存结果

保存数据文件： save session my.session
恢复之前保存的数据文件：restore session my.session

LEC实操

LEC启动方式

普通启动方式：lec -gxl （图像化界面）（用的更多）
纯命令行启动方式：lec -nogui -gxl
启动并运行写好的脚本：lec -gxl -dofile top_lec.tcl
打开或者关闭图形化界面：set gui on/off

流水线加法器形式验证

top_lec.do

set log file  ./top_lec.log -replacedofile ./script/set_env.doresetread library -Both -sensitive -Verilog /home/XXX/fab/synopsys90nm_lib/stdcel/verilog/saed90nm.vread design -systemverilog -Golden -sensitive  -root $working_design -file ./source_file/flist.fread design -systemverilog -Revised  -sensitive  -root $working_design ./source_file/syn.vset flatten model  -seq_merge -seq_constant  -SEQ_Redundant
set datapath option -auto -verbose
set analyze option -auto// add renaming rule a2 \[ _  -golden -type DFF
// add renaming rule a1 ] _  -golden -type DFF
set flatten model -seq_constant
set flatten model -latch_transparent
//
add pin constraints 0 RST  -Both// add pin constraints 0 SCAN_MODE_REG[0] -module scan_ctrl -Bothdofile ./script/lec_black_box.do// would map the invert phase
set mapping method -phaseset system mode lec // add mapped points top/a/b top/a/d  -noinvert
// analyze setup
analyze setup
remodel -seq_const -repeat
set mapping method -name first -phase -UNREACH
map key pointsadd compared points -allcompare > $RPT_OUT/lec_$working_design.logreport compare data > $RPT_OUT/lec_verbose_$working_design.log
report mapped points > $RPT_OUT/lec_mapped_points.rpt
report unmapped points > $RPT_OUT/lec_unmapped_points.rptreport black box -class Full -Both -Instance -Hier -Hidden > $RPT_OUT/lec_black_box.rpt
report statistics > $RPT_OUT/lec_statistics.rptsave session my.session

set_env.do


setenv file_version     cp_test
setenv working_design   plus_pipesetenv source_file      source_filesetenv RPT_DIR RPT
setenv OUT_DIR OUTsetenv RPT_OUT  $RPT_DIR/$file_version//$::env(RPT)
tclmode
if {[file exist RPT]} {echo "RPT already exist"
} else {system mkdir RPT
}
vpxmode// system mkdir ./RPT -f
system rm    ./RPT/$file_version -rf
system mkdir ./RPT/$file_version

补充：
formality软件使用教程

形式验证——学习笔记相关推荐

MATLAB simulink 模型验证学习笔记
MATLAB simulink 模型验证学习笔记一.静态验证 1.Model Advisor 模型验证意思是用matlab自带的规范检查工具来检查自己画的模型是否符合规范. 进行模型验证需要用到的模 ...
[Simulink] 基于模型的测试与验证学习笔记_Step 4：Testing By Simulation
文章目录仿真测试 Test Harness 创建Test Harness 导入测试用例构建Test Harness模型执行测试.分析结果利用SDI进行结果的验证 Model Verficati ...
[Simulink] 基于模型的测试与验证学习笔记_Step 3: Detecting Desig Errors
文章目录 Simulink Design Verifier 对模型做死逻辑检测问题分析模型除以零的检测自动设计错误检测总结 [注] 本文为2018 Mathworks 年会上机教程学习笔记, ...
MCDF验证学习笔记
文章目录前言 mcdf模块简介 mcdf验证结构布局测试用例覆盖率收集分析覆盖率收集情况添加新的测试用例异常激励测试前言本文仅个人学习过程笔记,如有疏漏,望指正或补充. mcdf模块简 ...
MyBatis collection的两种形式——MyBatis学习笔记之九
与association一样,collection元素也有两种形式,现介绍如下: 一.嵌套的resultMap 实际上以前的示例使用的就是这种方法,今天介绍它的另一种写法.还是以教师映射为例,修改映射 ...
[zz]ASP.NET MVC2框架验证学习笔记
ASP.NET中的框架验证方法1: 1.模型定义 public class User { [Required(ErrorMessage="用户名不能为空!!")] [ ...
琴生不等式一般形式_[学习笔记]常用不等式
1. 命题左边等号成立当且仅当 ,右边等号成立当且仅当 . 2. 命题等号成立当且仅当 . 3.命题两边等号成立均当且仅当 . 4.命题两边等号成立均当且仅当 . 推论 5. 命题 6. 不等 ...
IC验证学习笔记（MCDF）实验0-MCDT
实验0:目标是写出MCDT的程序,也就是slave+fifo+arbiter的部分最终目标是实现MCDF:MCDF为多通道数据整形器(multi-channel data formatter),它可 ...
MyBatis association的两种形式——MyBatis学习笔记之四
一.嵌套的resultMap 这种方法本质上就是上篇博文介绍的方法,只是把教师实体映射从association元素中提取出来,用一个resultMap元素表示.然后 association元素再引用 ...
mysql association_MyBatis association的两种形式——MyBatis学习笔记之四
一.嵌套的resultMap 这种方法本质上就是上篇博文介绍的方法,只是把教师实体映射从association元素中提取出来,用一个resultMap元素表示.然后 association元素再引用 ...

形式验证——学习笔记