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

通常情況下，形式驗證的工具的主戰(zhàn)場，是在RTLvsSYN這個階段，主要是由于綜合器的mapping/optimization會遇到各種各樣的挑戰(zhàn)。但是，本案有一些不同，在通常很容易的SYNvsLAY里邊，出現(xiàn)了一點小插曲。筆者整理了一下，以嗜各位讀者。
在ICC的結(jié)束以后，一般都會先走一個formal檢查，保證SYNvsLAY的一致性，通常都是一鍵過的，可是，在這個案子里邊，出現(xiàn)了下邊的問題：

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

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

經(jīng)過按步驟排查，發(fā)現(xiàn)問題竟然出現(xiàn)在CTS的一個命令里邊，有點撲朔迷離。DEBUG 安排！

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

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

可以看到，整個數(shù)據(jù)庫，被拿掉了235個buffers和4個inveters ?？磥磉€是有一定面積優(yōu)化的效果。

基本現(xiàn)象是：如果跳過這個命令，formal就沒有問題，反之就會有問題?？傆X得哪里不太對：一個buffer removing的動作，會引起FM的問題？

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

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

FM竟讓給了一個大大的suprise：FM相等！。buffer移除出錯了？
這個時候，還是仔細看看FM的log，注意到下面有趣的信息

log表明，由于DIODE_cell的DIODE pin是個INOUT，導(dǎo)致和它相連接的port被相應(yīng)轉(zhuǎn)成了INOUT方向。
通常，F(xiàn)M再比對的時候會通過IN/INOUT port給輸入port加入激勵。所以，這里的pt2out[5] port，雖然是一個輸出口，但是被FM改變成一個雙向口，會向里邊打入激勵。
但是，這個DIODE帶來的的影響，在不使用remove_clock_tree的數(shù)據(jù)庫里的情形是一樣的！看來，這個還不是root-cause。

繼續(xù)使用FM的analysis功能，

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

聰明的讀者一定想到了一點：是不是前邊的FM-579導(dǎo)致的問題呢？是的，你說對了，但是也只是對了一半！
還是回到ICC，通過all_fanin來看，pt2out[5]的driver都是干凈的，并沒有看到sar_clk，這個可以證明，的確是FM-579引起的問題，所以，如果移除DIODE pin的direction的問題。FM一定可以過。
但是，這么好的一個DEBUG機會，怎么可以就此放過。使用report_timing看看，就看到了另外一半的原因了。舒坦！

--------------------------------- TEA TIME -------------------------------
--------------------------------- TEA TIME -------------------------------先出場的FM不相等的數(shù)據(jù)庫
先看一下到sar_clk的timing path：可以看到，這個port 有一個**…G4IP/Z buffer驅(qū)動。沒有什么問題。但是，請留意一下黃色高亮區(qū)域的這個net：…/inst_SAR/sar_clk (net)**

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

既然都花了這么久的debug功夫，也不介意再看一下，正確網(wǎng)表：沒有使用remove_clock_tree命令的網(wǎng)表FM可以pass的原因了。
還是看一下ICC的timing report。對于FM而言，這里的sar_clk port 還是一個輸入激勵端，但是可以看到，這里的sar_clk的網(wǎng)表driver 是一個BUF/Z（place239/Z），按照lib的定義BUF是不能反向傳遞的，所以，F(xiàn)M-579的影響，到place239這里就截止了（注意到，place239/Z的負載只有一個），并不會影響其他的地方。

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

• 剔除DIODE cell的DIODE pin的雙向口影響：導(dǎo)出netlist 的時候 ，使用 write_verilog -no_diode_port 選項，F(xiàn)M不會出現(xiàn)FM-579的問題

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