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

形式验证 formality的设置及fm_shell使用形式验证进阶(二):Setup阶段的约束信息&说说formality中比较点匹配2018-10-26芯司机公众号:chipdriver之前的文章导读《形式验证入门之基本概念和流程》《形式验证进阶

形式验证进阶(二):Setup阶段的约束信息&说说formality中比较点匹配

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

形式验证 formality的设置及fm_shell使用
之前的文章导读
《形式验证入门之基本概念和流程》
《形式验证进阶(一):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来匹配。
形式验证 formality的设置及fm_shell使用
图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的设置,并自动分析门控结构。
形式验证 formality的设置及fm_shell使用
图2.1
形式验证 formality的设置及fm_shell使用
图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推导,这样会浪费大量的时间。
形式验证 formality的设置及fm_shell使用
图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之间的一致性验证。
形式验证 formality的设置及fm_shell使用
如果综合工具不是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的使用问题
形式验证 formality的设置及fm_shell使用
图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命令后,验证通过的概率是很大的。
形式验证 formality的设置及fm_shell使用
福利
回复“领取资料”关键词即可获取IC资料包
形式验证 formality的设置及fm_shell使用
 

分享连接:
http://m.5stu.com/f97584.html

今天的文章形式验证 formality的设置及fm_shell使用分享到此就结束了,感谢您的阅读。

版权声明:本文内容由互联网用户自发贡献,该文观点仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 举报,一经查实,本站将立刻删除。
如需转载请保留出处:https://bianchenghao.cn/63201.html

(0)
编程小号编程小号

相关推荐

发表回复

您的电子邮箱地址不会被公开。 必填项已用*标注