121.Formality设置和比较点匹配问题
2020-06-18 14:34阅读：
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）时钟线路上插入buffer前和插入buffer后，寄存器时钟pin连接的时钟线名称有变，需要使用set_user_match来匹配clk和clk1、clk2和clk3，如果时钟线路插入的是反相器，那么使用set_user_match
–inverter来匹配。
5）综合后PowerCompiler会插入门控，而将电路实现为图2.2的电路结构，该实现电路结构中由于引入latch，而会引入新的比较点，且寄存器时钟输入结构也有所变化，这会引起不匹配问题。解决的办法是：a）根据门控结构设置变量verification_clock_gate_hold_mode，如果是latch-and结构门控，那么该变量设置为low，如果是latch-or结构门控，那么该变量设置为high，如果两种结构都使用了，那么该变量设置为any；b）设置verification_clock_gate_edge_analysis变量为真，formality工具会忽略变量verification_clock_gate_hold_mode的设置，并自动分析门控结构。
6）综合时会出现inversi
on push现象，这时会引起verify
fail，需要对这种情况加以说明，声明的方式有两种：a）使用set_inv_push命令，将ref设计中的寄存器，反转极性加以说明；b）使用set_user_match命令声明两个比较点是匹配点且极性关系为反向，相比set_inv_push，set_user_match有更高的优先级。c）慎重使用变量verification_inversion_push，一旦该变量使能，在verify时，对所有不匹配点都会去做inversion
push推导，这样会浪费大量的时间。
7）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优化的情况有三种：a）使用set_optimize_registers命令对允许进行register retiming
的寄存器施加set_optimize_registers属性，然后使用compile_ultra命令触发优化。这种综合方法和传统综合方式相同，只需要生成一个SVF文件即可。b）使用compile_ultra
–retime命令触发优化。c）在compile_ultra命令后，再使用optimize_register命令触发优化。第（b）种和第（c）种情况下，每次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之间的一致性验证。
![]( "121.Formality设置和比较点匹配问题")
如果综合工具不是DC，那么在formality中使用set_parameters -retimed
designID命令声明哪个设计中做了register retiming。
8）除了常数值设置，有时一个逻辑锥的某几个输入之间是有某种组合关联的，声明这些输入的相互关系，称为设置约束。根据约束，formality只用符合要求的激励做验证，从而减少了验证时间、降低了验证失败概率。用户可以使用set_constraint命令来设置约束，典型的约束类型有：a）one-hot，只有一个输入为1，其他关联输入为0；b）one-cold，只有一个输入为0，其他关联输入为1；c）Coupled：几个相关联的输入值是相同的；d）Mutually
exclusive，两个输入点的值处于相反的状态。Formality中共有8种预定义类型，用户也可以定义新的约束类型。首先需要通过写module来表述几个输入的间关系，该module可以有多个输入，但只能有一个输出，输出为1表示输入符合要求，输出为0表示输入不符合要求，且该module中不能出现黑盒子、双向端口、三态逻辑和时序单元。
设计人员还是需要考虑fsm采用何种编码更合适的，而形式验证中fsm
re-encoding很少见，如果一旦遇到可以查找formality和design
compiler用户手册，里面对一些极少出现的情况专门作了说明，这里也不再赘言。
9）说说formality中比较点匹配
*触发formality比较点匹配的命令
触发比较点匹配的方式有两种：a）执行命令verify时，formality会先自动对未成功匹配的比较点先进行匹配，然后再针对比较点做一致性验证；b）使用match命令执行比较点匹配操作。常用的操作方式是match
— report_unmatched_points —undo_match— make some changes —
match循环操作，直到符合要求为止。这里需要说明：a）match和verify命令都是只对未成功匹配的比较点进行匹配，已经匹配的比较点不再重新匹配；b）undo_match只是撤销最近一次执行的match命令，undo_match
–all会将所有比较点退回到未匹配状态。
*formality进行比较匹配遵循的规则
a) Exact-name matching，相关控制变量：name_match
all
b) Name filtering
将名称中诸如“+[]”等变量name_match_filter_chars包含符号替换成“_”后，再基于名称进行大小写不敏感的匹配
相关控制变量：
name_match_use_filter true
name_match_filter_chars‘~!@#$%^&*()_+=|\{}[]”:;<>?,./
c)
Topological equivalence
不基于名称的匹配，如果驱动两个比较点的逻辑锥等价，那么这两个比较点等价
d) Signature analysis
不基于名称的匹配，一种针对比较点的迭代分析算法，很费时
相关控制变量：
signature_analysis_match_datapath true
signature_analysis_match_hierarchy true
signature_analysis_match_compare_points
true
e) Compare point matching based on net
names
连接比较点的net同名，那么这两个比较点匹配
相关控制变量：
name_match_based_on_nets true
10)
如何debug未能匹配的比较点
a）reference design和implementation
design中不匹配点的数目相同么？如果相同，那么按理可能的原因是DC优化时改变了比较点名称，这时可使用set_user_match命令人工帮助比较点匹配。
b）报告中是否有Und、BBPIN和BBOX问题的提示？如果有，那么要首先解决黑盒子问题。可使用report_black命令报告黑盒子信息，如果reference
design或implementation
design中存在unresolved原因而生成的黑盒子，这通常会引起比较点不匹配，进而影响verify。
c）报告中是否有LATCH0等常值提示和LATCHCG的门控提示？如果reference
design中有常值LATCH或者DFF，而implementation
design中没有，这是因为DC会将常值器件优化掉的缘故；如果只有implementation
design中有LATCHCG提示，而reference design中没有，那很可能是DC在综合时，power
compiler自动插入门控单元的原因。以上两种情况都可以暂且不处理，执行verify命令后，如果验证通过，那么忽略这些不匹配信息，如果验证失败，那么可以结合这些信息进一步分析原因。
d）若RTL中使用了compile指令full_case和parallel_case，而代码风格不好，那么就会造成仿真和综合不一致的问题，最典型的情况如下表所示。这时，如果在使用formality工具时，设置hdlin_ignore_full_case
= false和hdlin_ignore_parallel_case =
false，一致性比对就会通过。个人建议尽量使用case语句，而少用casez和casex语句.
这里再重复一下重点：a）如果是先做了block级综合，再在顶层综合，那么不要直接做顶层验证，而是先做block级验证，然后用验证通过的网表做输入，再进行顶层验证；b）做好基本的几个变量的设置：hdlin_dwroot、verification_clock_gate_hold_mode、verification_set_undriven_signals、verification_inversion_push、hdlin_unresolved_modules
；c）做好setup和match处理，一定要先保证formality版本和dc版本的兼容性和svf文件版本准确性，如果实在无法match，再使用set_user_match和set_compare_rule处理。
引用：
https://blog.csdn.net/cy413026/article/details/87206033
