Formality：Bug记录

相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482本文记录博主在使用Synopsys的形式验证工具Formality中遇到的一个Bug。Bug复现情况一// 例1 module dff ( input clk, input d_in, output d_out ); reg q1, q2; always (posedge clk) begin q1 d_in; q2 q1; end assign d_out q2; endmodule首先以例1的RTL代码作为参考设计和实现设计然后在setup模式使用以下set_constant命令使得q1、q2触发器变成不可读触发器。set_constant -type net r:/WORK/dff_chain/d_out 1 set_constant -type net i:/WORK/dff_chain/d_out 1关于不可读的更详细信息可以参考下面的博客。Formality不可读(unread)的概念https://chenzhang.blog.csdn.net/article/details/145242304随后在fm_shell中使用match命令进行匹配或在GUI界面点击Run Matching此时fm_shell中显示的匹配结果与GUI界面显示的匹配结果出现了差别如下所示。// fm_shell的匹配结果 *********************************** Matching Results *********************************** 1 Compare points matched by name 0 Compare points matched by signature analysis 0 Compare points matched by topology 0 Matched primary inputs, black-box outputs 0(0) Unmatched reference(implementation) compare points 0(0) Unmatched reference(implementation) primary inputs, black-box outputs ****************************************************************************************// GUI界面的匹配结果 3 points matched by name 0 points matched by signature analysis 0 points matched by topology 0 points matched by user 0 unmatched reference points 0 unmatched implementation points结果显示fm_shell没有考虑两对匹配的不可读触发器而GUI界面考虑了更严重的是此时输入/输出端口没有显示在任何匹配报告中。这对最后的验证结果没有影响不可读触发器在默认情况下会被归为Not Compared类而不进行验证可通过verification_verify_unread_compare_points变量改变如下所示。********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/dff_chain Implementation design: i:/WORK/dff_chain 1 Passing compare points ---------------------------------------------------------------------------------------- Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL ---------------------------------------------------------------------------------------- Passing (equivalent) 0 0 0 0 1 0 0 1 Failing (not equivalent) 0 0 0 0 0 0 0 0 Not Compared Unread 0 0 0 0 0 2 0 2 ****************************************************************************************情况二以例2的RTL代码的作为实现设计而使用例1的RTL代码作为参考设计匹配结果如下所示。// 例2 module dff ( input clk, input d_in, output d_out ); reg q1, q2, q3; always (posedge clk) begin q1 d_in; q3 d_in; q2 q1; end assign d_out q2; endmodule// fm_shell的匹配结果 *********************************** Matching Results *********************************** 3 Compare points matched by name 0 Compare points matched by signature analysis 0 Compare points matched by topology 2 Matched primary inputs, black-box outputs 0(0) Unmatched reference(implementation) compare points 0(0) Unmatched reference(implementation) primary inputs, black-box outputs 1(0) Unmatched reference(implementation) unread points ****************************************************************************************// GUI界面的匹配结果 5 points matched by name 0 points matched by signature analysis 0 points matched by topology 0 points matched by user 0 unmatched reference points 0 unmatched implementation points结果显示fm_shell的匹配结果中列出了这个未匹配的不可读触发器而输入/输出端口显示在了匹配报告中。情况三以例2的RTL代码作为参考设计和实现设计匹配结果如下所示。// fm_shell的匹配结果 *********************************** Matching Results *********************************** 3 Compare points matched by name 0 Compare points matched by signature analysis 0 Compare points matched by topology 2 Matched primary inputs, black-box outputs 0(0) Unmatched reference(implementation) compare points 0(0) Unmatched reference(implementation) primary inputs, black-box outputs ****************************************************************************************// GUI界面的匹配结果 6 points matched by name 0 points matched by signature analysis 0 points matched by topology 0 points matched by user 0 unmatched reference points 0 unmatched implementation points结果显示fm_shell没有考虑这对匹配的不可读触发器而GUI界面考虑了而输入/输出端口显示在了匹配报告中。Bug总结1、当使用set_constant命令导致不可读触发器时fm_shell和GUI界面的匹配结果不一致输入输出端口不会出现在任何匹配报告中而匹配的不可读触发器不出现在fm_shell中对最终验证没有影响。2、即使不使用set_constant命令fm_shell和GUI界面的匹配结果也不一致匹配的不可读触发器不出现在fm_shell中对最终验证没有影响。Bug反馈目前已在Solvnet上向Synopsys提出反馈如下图所示。