在當前的形式驗證的領域，主要有兩個工具，一個就是Cadence的conformal，另外一個就是Synopsys的formality（以下簡稱FM）。

通常情況下，形式驗證的工具的主戰場，是在RTLvsSYN這個階段，主要是由于綜合器的mapping/optimization會遇到各種各樣的挑戰。但是，本案有一些不同，在通常很容易的SYNvsLAY里邊，出現了一點小插曲。筆者整理了一下，以嗜各位讀者。

在ICC的結束以后，一般都會先走一個formal檢查，保證SYNvsLAY的一致性，通常都是一鍵過的，可是，在這個案子里邊，出現了下邊的問題：

可以看到，有1個BBnet和1個BBpin的不等。展開GUI，可以看到如下的提示：

可以看到，有一個是DIODE cell的DIODE pin 不相等，另外一個是和這個DIODE cell 相連接的net 不等，這個net也是會送到對應的output port的 ，如下圖所示

經過按步驟排查，發現問題竟然出現在CTS的一個命令里邊，有點撲朔迷離。DEBUG 安排！

在ICC的``步驟里邊，CTS階段，為了節省面積，使用了下邊這個命令

在命令結束的地方，有一些小結，可以看到一些冗余的buffer/inveter被拿掉了

可以看到，整個數據庫，被拿掉了235個buffers和4個inveters。看來還是有一定面積優化的效果。

基本現象是：如果跳過這個命令，formal就沒有問題，反之就會有問題。總覺得哪里不太對：一個buffer removing的動作，會引起FM的問題？

為了定位問題，將上邊的remove_clock_tree命令分解，可以定位出來，如果使用下面的細化命令，是會引起這個FM的問題。

難道是inverter出的問題！來來來，把buffer全部dont_touch：

FM竟讓給了一個大大的suprise：FM相等！。buffer移除出錯了？

這個時候，還是仔細看看FM的log，注意到下面有趣的信息

log表明，由于DIODE_cell的DIODE pin是個INOUT，導致和它相連接的port被相應轉成了INOUT方向。

通常，FM再比對的時候會通過IN/INOUT port給輸入port加入激勵。所以，這里的pt2out[5] port，雖然是一個輸出口，但是被FM改變成一個雙向口，會向里邊打入激勵。

但是，這個DIODE帶來的的影響，在不使用remove_clock_tree的數據庫里的情形是一樣的！看來，這個還不是root-cause。

繼續使用FM的analysis功能，

可以看到，這里的Cone Input有一個很奇怪的地方，這里的sar_clk在設計里邊是一個output port，怎么會成為影響到另外一個output port pt2out[5]的Unmatched Cone input呢？

聰明的讀者一定想到了一點：是不是前邊的FM-579導致的問題呢？是的，你說對了，但是也只是對了一半！

還是回到ICC，通過all_fanin來看，pt2out[5]的driver都是干凈的，并沒有看到sar_clk，這個可以證明，的確是FM-579引起的問題，所以，如果移除DIODE pin的direction的問題。FM一定可以過。

但是，這么好的一個DEBUG機會，怎么可以就此放過。使用report_timing看看，就看到了另外一半的原因了。舒坦！

先出場的FM不相等的數據庫

先看一下到sar_clk的timing path：可以看到，這個port 有一個**…G4IP/Z buffer驅動。沒有什么問題。但是，請留意一下黃色高亮區域的這個net：…/inst_SAR/sar_clk (net)**



再看一下到pt2out[5]的timing path：可以看到，這個port 有一個…G4IP/Z buffer驅動。沒有什么異樣，但是，請注意黃色方塊高亮區域，這個net就是上邊timing report的高亮的那個net！所以，從FM的角度來看pt2out[5]的driver，在版圖的網表里邊，有兩個driver：…G4IP/Z 和 sar_clk。這個就是FM的根本原因。



既然都花了這么久的debug功夫，也不介意再看一下，正確網表：沒有使用remove_clock_tree命令的網表FM可以pass的原因了。

還是看一下ICC的timing report。對于FM而言，這里的sar_clk port 還是一個輸入激勵端，但是可以看到，這里的sar_clk的網表driver 是一個BUF/Z（place239/Z），按照lib的定義BUF是不能反向傳遞的，所以，FM-579的影響，到place239這里就截止了（注意到，place239/Z的負載只有一個），并不會影響其他的地方。



在沒有使用remove_clock_tree的數據庫里邊，由于place239這個buffer的保護，FM-579的影響并沒有傳遞到合法的比較點上，所以FM是可以過的。反之，則會影響到FM的結果。
敲黑板的時間到了，解決方案如下

剔除DIODE cell的DIODE pin的雙向口影響：導出netlist 的時候 ，使用write_verilog -no_diode_port選項，FM不會出現FM-579的問題

在input/output PORT 添加隔離buffer，阻斷DIODE的FM誤動作。

審核編輯：劉清