Formality：Bug记录

相关阅读

Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482

---

        本文记录博主在使用Synopsys的形式验证工具Formality中遇到的一个Bug。

Bug复现

情况一

// 例1
module dff (input clk,    input d_in,      output d_out    
);reg q1, q2;  always @(posedge clk) beginq1 <= d_in;  q2 <= q1;       endassign 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 name0 Compare points matched by signature analysis0 Compare points matched by topology0 Matched primary inputs, black-box outputs0(0) Unmatched reference(implementation) compare points0(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_chainImplementation design: i:/WORK/dff_chain1 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 ComparedUnread                       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) beginq1 <= d_in;  q3 <= d_in; q2 <= q1;       endassign d_out = q2;
endmodule

// fm_shell的匹配结果
*********************************** Matching Results ***********************************3 Compare points matched by name0 Compare points matched by signature analysis0 Compare points matched by topology2 Matched primary inputs, black-box outputs0(0) Unmatched reference(implementation) compare points0(0) Unmatched reference(implementation) primary inputs, black-box outputs1(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 name0 Compare points matched by signature analysis0 Compare points matched by topology2 Matched primary inputs, black-box outputs0(0) Unmatched reference(implementation) compare points0(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提出反馈，如下图所示。