1. 为什么要formal verification
比较两个design的function是否一致
RTL 功能正确: function verifiation: UVM testbench + simulation
工具: system
verilog, UVM, VCS, NCSim
1.1 比较对象
RTL Vs Pre
layout_Netlist,
prelayout_netlist Vs post_p&R _netlist
post_p&R_netlist Vs detail_route_netlist
1.2 术语
reference design: 功能正确,作为比对正确的参照物,又称在golden
implementation design: 设计过程中改变过的design,是检查的对象
container: design和libraries的database, 包括了Hard macro,综合用的标准库
默认的reference container的名字是r
默认的implementation container的名字是i
design的信息可以保存在container里面,下次可以直接读入container
1.3 reference design假定是功能正确的
formality用来检查implemation design是否和reference design一致
是采用数学方法进行穷尽检查的一种比对的方法,没有corner case
不需要test vector, design转化成logic cones的连接
通过算法在每个logic cone的输入加上激励,比较输出是否一致,并不需要test vector
1.4 compare points: primary output, Register或latch的输出,bbox的input
还有一些其它的不常用的比对点: 多驱动的net,组合逻辑环的cutpoint
1.5 logic cone:
输入可以时Primary Input, 寄存器或锁存器的输出, BBOX的Output pin
输出是compare points
formality把design分割成logic cone
2. Flow Overview
2.1 Partition: 把reference和implementation design分割成logic cones和compare points
Read Reference design(REF), implementate design(IMP) and libary(LIB)
2.2 Match: 把REF和IMP中的compare points建立映射关系
实际操作中,大多数的comare points是通过名字来match的,例如a_reg[31] Vs a_reg_31_
否则,需要guidance information, 手动指定match或比对的规则(rule)
所以,match的结果是: 紫色代表matched cone, 绿色代表用户定义的matched cone,红色代表unmatched cone
2.3 verify: 检查每对compare points的逻辑功能是否一致
结果: 黑色代表passing cone, 红色代表failing cone, 蓝色代表unmatched cone
对于unmatched cone,可以设成不要比对(但结果可能不正确)
2.4 Debug: 有GUI方式和report的方式
在match或verify的阶段,如果有unmatched或failed cone,就要进行debug
一种是使用GUI的方式,打开对应的unmatched或failed cone,检查是否一致
也可以在input pattern list中选择pattern,加到logic cone的input pin上,检查逻辑是否一致
3. 使用formality
3.1 启动
a. batch mode: fm_shell -gui -f runme.fms | tee runme.log
b. gui: formality
c. 在batch mode启动GUI: fm_shell(setup) > start_gui
d. 查看帮助文件: fm_shell -help
3.2 加载guidance
综合时,DC会自动生成一个svf文件,其中记录了一些优化后的信息,例如被去除的逻辑,被改名的寄存器
formality可以通过svf获得更好的match
"set_svf default.svf"
3.3 读入reference design + libs + "set_top",使用"-r"的选项
set_top可以设置要检查的最顶层,并且进行elaborate把top level下的design自动构建起来
"read_verilog -r alu.v"
"set_top alu"
3.4 读入implementation design + libs + "set_top",使用"-i"的选项
"read_db -i lsi_10k.db"
"read_verilog -i alu.fast.vg"
"set_top -auto"
3.5 setup
做一些setting. 例如,implementation中会包含
DFT的信息,而RTL并没有这一部分,必须mask,不对这部分进行比对
例如JTAG, SCAN的逻辑
3.6 match & verify
a.
b. 可以省略match, 直接"verify",这个命令可以做match+verify
3.8 debug