相關閱讀

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提出反饋，如下圖所示。