形式验证 formality的设置及fm_shell使用

形式验证进阶（二）：Setup阶段的约束信息&说说formality中比较点匹配

2018-10-26 芯司机公众号：chipdriver

之前的文章导读
《形式验证入门之基本概念和流程》
《形式验证进阶（一）：Guidance&Load Design》
Setup阶段的约束信息
1．常规setup设置
1）如果DC的综合脚本中使用了set_case_analysis命令，那么在formality中使用set_constant命令对相应的port、pin、net或者register cell也设置为常数。2）使用set_constant命令将testmode设置为功能模式，将scan_enable设置为无效，从而disablescan logic。3）使用set_constant命令disable边界扫描。4）如图1所示，时钟线路上插入buffer前和插入buffer后，寄存器时钟pin连接的时钟线名称有变，需要使用set_user_match来匹配clk和clk1、clk2和clk3，如果时钟线路插入的是反相器，那么使用set_user_match –inverter来匹配。

图1. 时钟线插入buffer示意图
5）如图2所示，RTL描述的是图2.1的电路结构，综合后PowerCompiler会插入门控，而将电路实现为图2.2的电路结构，该实现电路结构中由于引入latch，而会引入新的比较点，且寄存器时钟输入结构也有所变化，这会引起不匹配问题。解决的办法是：1）根据门控结构设置变量verification_clock_gate_hold_mode，如果是latch-and结构门控，那么该变量设置为low，如果是latch-or结构门控，那么该变量设置为high，如果两种结构都使用了，那么该变量设置为any；2）设置verification_clock_gate_edge_analysis变量为真，formality工具会忽略变量verification_clock_gate_hold_mode的设置，并自动分析门控结构。

图2.1

图2.2
6）如图3所示，综合时会出现inversion push现象，这时会引起verify fail，需要对这种情况加以说明，声明的方式有两种：1）使用set_inv_push命令，将ref设计中的寄存器，反转极性加以说明；2）使用set_user_match命令声明两个比较点是匹配点且极性关系为反向，相比set_inv_push，set_user_match有更高的优先级。3）慎重使用变量verification_inversion_push，一旦该变量使能，在verify时，对所有不匹配点都会去做inversion push推导，这样会浪费大量的时间。

图3. Inversion push说明图
2. retime design的验证
Register retiming是为了满足时序或者面积需求，而将寄存器跨组合逻辑移动，这种移动可能会改变寄存器的数量和寄存器连接关系，进而引起综合出来的implementation design和reference design比较点匹配不上，所以这种优化手段通常并不建议一开始就使用，如果确实收敛困难，那么再采用这种优化手段。这时，需要在setup阶段，向formality提供register retiming信息，以帮助formality进行match和verify操作。如果采用的综合工具是DC，那么恰当的生成SVF文件，并将SVF文件提供给formality，若formality中变量svf_retiming使能（该变量默认即为真），便可以自动处理SVF文件中guide_retiming相关命令，并通过向reference design中插入黑盒子产生断点的方式来帮助比较点匹配。下面再说说，关于SVF文件的生成和使用。
触发DC工具进行register retiming优化的情况有三种：1）使用set_optimize_registers命令对允许进行register retiming 的寄存器施加set_optimize_registers属性，然后使用compile_ultra命令触发优化。这种综合方法和传统综合方式相同，只需要生成一个SVF文件即可。2）使用compile_ultra –retime命令触发优化。3）在compile_ultra命令后，再使用optimize_register命令触发优化。第（2）种和第（3）种情况下，每次DC使用compile_ultra –retime命令或optimize_register命令前，都要配置SVF文件，每次命令执行后写出网表信息，并将SVF文件和生成的网表交给formality进行一致性验证。DC脚本举例如下所示，其中，文件compile_1.svf辅助rtl.v和compile_1.ddc之间的一致性验证；文件compile_2.svf辅助compile_1.ddc和compile_2.ddc之间的一致性验证；文件compile_3.svf辅助compile_2.ddc和compile_3.ddc之间的一致性验证。

如果综合工具不是DC，那么在formality中使用set_parameters -retimed designID命令声明哪个设计中做了register retiming。
3、使用外部约束
除了常数值设置，有时一个逻辑锥的某几个输入之间是有某种组合关联的，声明这些输入的相互关系，称为设置约束。根据约束，formality只用符合要求的激励做验证，从而减少了验证时间、降低了验证失败概率。用户可以使用set_constraint命令来设置约束，典型的约束类型有：1）one-hot，只有一个输入为1，其他关联输入为0；2）one-cold，只有一个输入为0，其他关联输入为1；3）Coupled：几个相关联的输入值是相同的；4）Mutually exclusive，两个输入点的值处于相反的状态。Formality中共有8种预定义类型，用户也可以定义新的约束类型。首先需要通过写module来表述几个输入的间关系，该module可以有多个输入，但只能有一个输出，输出为1表示输入符合要求，输出为0表示输入不符合要求，且该module中不能出现黑盒子、双向端口、三态逻辑和时序单元。
module my_2hot(in1,in2,in3,out);
input in1,int2,in3;
output out;
always @*
case ({in1,in2,in3})
3’b110: out = 1;
3’b101: out = 1;
3’b011: out = 1;
default: out = 0;
endcase
endmodule
fm_shell > create_container rel
fm_shell > read_verilog –container rel my_2hot.v
fm_shell >create_constraint_type 2hotrel:/WORK/my_2hot
fm_shell >set_constraint2hot {Q_reg[0] Q_reg[1] Q_reg[2]} –map {in1=Q_reg[0] in2=Q_reg[1] in3=Q_reg[2]} rel:/WORK/mytest
如上所示，通过定义modulemy_2hot表述三个输入，必有两个高电平和一个低电平这样的关系，然后将该模块读入，并通过create_constraint_type命令产生新的约束类型2hot，再使用set_constraint命令来约束设计mytest中的Q_reg允许的组合值的范围。
4、有限状态机重编码
事实上，这种情况很少见，而Lynn还在此特别说明是因为，当Lynn还是小小司机初次做项目写代码时，Lynn的前辈告诉Lynn，写代码不用太注意状态机编码，现在DC都可以对此进行优化了，所以很长一段时间，Lynn都是清一色对状态机采用普通二进制编码的。不过，DC在优化过程中默认是不会对fsm重新编码的，但是DC工具确实是有这样的功能的，只是实际综合时，经验少的综合人员甚至不知道这个功能，知道这个功能的综合人员也基本不会采用这种策略来优化设计，大概的原因是：1）全局提取fsm信息，然后采用统一编码的策略有可能影响设计的可靠性，毕竟很多设计的编码策略是经过慎重考虑的，是有要求的，比如双端口FIFO设计；2）需要局部的具有针对性的改变编码策略也很少见，因为很少遇到关键路径是因为状态机编码风格才时序紧张的；3）改变fsm编码，增加了形式验证的难度。也就是说，设计人员还是需要考虑fsm采用何种编码更合适的，而形式验证中fsm re-encoding很少见，如果一旦遇到可以查找formality和design compiler用户手册，里面对一些极少出现的情况专门作了说明，这里也不再赘言。
说说formality中比较点匹配
1、触发formality比较点匹配的命令
触发比较点匹配的方式有两种：1）执行命令verify时，formality会先自动对未成功匹配的比较点先进行匹配，然后再针对比较点做一致性验证；2）使用match命令执行比较点匹配操作。常用的操作方式是match — report_unmatched_points —undo_match— make some changes — match循环操作，直到符合要求为止。这里需要说明：1）match和verify命令都是只对未成功匹配的比较点进行匹配，已经匹配的比较点不再重新匹配；2）undo_match只是撤销最近一次执行的match命令，undo_match –all会将所有比较点退回到未匹配状态。
2、formality进行比较匹配遵循的规则
如下表所示，比较点匹配的方式可分为五种，formality按照优先级从高到低的顺序，逐步采用相关算法针对未匹配成功的比较点进行匹配，绿色区域表示匹配方式是基于名称的，蓝色区域表示匹配方式是不基于名称的。
优先级
匹配方式
解释
1
Exact-name matching
1）比较名称相同，匹配成功（大小写敏感）
2）大小写不敏感的，基于名称的匹配
相关控制变量：name_match all
2
Name filtering
将名称中诸如“+[]”等变量name_match_filter_chars包含符号替换成“_”后，再基于名称进行大小写不敏感的匹配
相关控制变量：
name_match_use_filter true
name_match_filter_chars‘~!@#$%^&*()_+=|\{}[]”:;<>?,./
3
Topological equivalence
不基于名称的匹配，如果驱动两个比较点的逻辑锥等价，那么这两个比较点等价
4
Signature analysis
不基于名称的匹配，一种针对比较点的迭代分析算法，很费时
相关控制变量：
signature_analysis_match_datapath true
signature_analysis_match_hierarchy true
signature_analysis_match_compare_points true
5
Compare point matching based on net names
连接比较点的net同名，那么这两个比较点匹配
相关控制变量：
name_match_based_on_nets true
3、如何debug未能匹配的比较点
Reference design和implementation design中存在unmatched compare points通常是由于DC优化过程中改变了比较点名称和数量所致，比如group和ungroup操作会改变设计层次以及接口命名，常值寄存器在优化过程中会被删除，寄存器复制会增加implementation design中比较点，power compiler会在implementation design中插入reference design中没有的门控时钟单元等。使用DC输出的.svf文件中的信息来帮助formality进行比较点匹配的方式很有效，这时，若仍有无法匹配点的点需要进一步做如下分析。
1）reference design和implementation design中不匹配点的数目相同么？如果相同，那么按理可能的原因是DC优化时改变了比较点名称，这时可使用set_user_match命令人工帮助比较点匹配。但其实，这种情况其实很少见，因为svf文件中的信息，一般足以帮助formality解决因为名称变化使得比较点无法匹配的问题，这时建议查看formality.log文件，看看svf信息是否有大量被拒绝的现象。如果有的话，需要检查svf文件设置的正确性、svf版本和网表版本的一致性，以及formality版本和DC版本之间的协调性。
2）报告中是否有Und、BBPIN和BBOX问题的提示？如果有，那么要首先解决黑盒子问题。可使用report_black命令报告黑盒子信息，如果reference design或implementation design中存在unresolved原因而生成的黑盒子，这通常会引起比较点不匹配，进而影响verify。具体的黑盒子方法设置可以参考Lynn先前的文章《简述Load design》。
3）报告中是否有LATCH0等常值提示和LATCHCG的门控提示？如果reference design中有常值LATCH或者DFF，而implementation design中没有，这是因为DC会将常值器件优化掉的缘故；如果只有implementation design中有LATCHCG提示，而reference design中没有，那很可能是DC在综合时，power compiler自动插入门控单元的原因。以上两种情况都可以暂且不处理，执行verify命令后，如果验证通过，那么忽略这些不匹配信息，如果验证失败，那么可以结合这些信息进一步分析原因。
4）若RTL中使用了compile指令full_case和parallel_case，而代码风格不好，那么就会造成仿真和综合不一致的问题，最典型的情况如下表所示。这时，如果在使用formality工具时，设置hdlin_ignore_full_case = false和hdlin_ignore_parallel_case = false，一致性比对就会通过。说到这里，补充一点题外话，1）在DC中的elaborate命令执行的log中是有case语句的解析信息的，这些信息以info形式给出，很容易让人忽略，如图1所示，如果显示fullauto，那么代表RTL分支表达完整，如果显示fullno，那么建议review一下代码；2）casez和casex语句的使用，很容易造成多重匹配，elaborate命令执行的log中若显示parallel no那么证明存在多重匹配，且产生优先级逻辑，至于这个优先级到底是冗余逻辑还是设计需求，那要看设计意图了，个人建议尽量使用case语句，而少用casez和casex语句。
compile指令
full_case
parallel_case
指令作用
指示综合工具，不用管case未提到的状态
指示综合工具，此电路无优先级逻辑
RTL风格
使用case语句，但是分支表达不全，且未用default分支
使用case、casez或casex语句，且存在多重匹配
仿真工具分析结果
分支不全，产生latch
多重匹配，产生优先级逻辑
综合工具综合结果
不全的分支，认为无关，无latch
无优先级逻辑
形式验证结果
有unmatched points，
verify fail
verify fail
表2 full_case 和parallel_case的使用问题

图1
5）利用图形界面debug，使用start_gui命令启动图形界面，利用图形界面可以查看电路原理图，formality的图形界面操作十分简单便捷，这里不多赘言。小结：Lynn从《形式验证的流程和基本概念》到《说说formality中比较点匹配》做了一个系列关于formality rtl2gate的分享，比较全面的介绍了新手如何独立完成formality rtl2gate的验证。这里再重复一下重点：1）如果是先做了block级综合，再在顶层综合，那么不要直接做顶层验证，而是先做block级验证，然后用验证通过的网表做输入，再进行顶层验证；2）做好基本的几个变量的设置：hdlin_dwroot、verification_clock_gate_hold_mode、verification_set_undriven_signals、verification_inversion_push、hdlin_unresolved_modules ；3）做好setup和match处理，一定要先保证formality版本和dc版本的兼容性和svf文件版本准确性，如果实在无法match，再使用set_user_match和set_compare_rule处理。做好以上三点，执行verify命令后，验证通过的概率是很大的。

福利
回复“领取资料”关键词即可获取IC资料包