淺析Formality形式驗(yàn)證里的案件

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

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

在ICC的結(jié)束以后，一般都會(huì)先走一個(gè)formal檢查，保證SYNvsLAY的一致性，通常都是一鍵過的，可是，在這個(gè)案子里邊，出現(xiàn)了下邊的問題：

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

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

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

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

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

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

基本現(xiàn)象是：如果跳過這個(gè)命令，formal就沒有問題，反之就會(huì)有問題。總覺得哪里不太對(duì)：一個(gè)buffer removing的動(dòng)作，會(huì)引起FM的問題？

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

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

FM竟讓給了一個(gè)大大的suprise：FM相等！。buffer移除出錯(cuò)了？

這個(gè)時(shí)候，還是仔細(xì)看看FM的log，注意到下面有趣的信息

log表明，由于DIODE_cell的DIODE pin是個(gè)INOUT，導(dǎo)致和它相連接的port被相應(yīng)轉(zhuǎn)成了INOUT方向。

通常，F(xiàn)M再比對(duì)的時(shí)候會(huì)通過IN/INOUT port給輸入port加入激勵(lì)。所以，這里的pt2out[5] port，雖然是一個(gè)輸出口，但是被FM改變成一個(gè)雙向口，會(huì)向里邊打入激勵(lì)。

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

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

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

聰明的讀者一定想到了一點(diǎn)：是不是前邊的FM-579導(dǎo)致的問題呢？是的，你說對(duì)了，但是也只是對(duì)了一半！

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

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

先出場(chǎng)的FM不相等的數(shù)據(jù)庫

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



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



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

還是看一下ICC的timing report。對(duì)于FM而言，這里的sar_clk port 還是一個(gè)輸入激勵(lì)端，但是可以看到，這里的sar_clk的網(wǎng)表driver 是一個(gè)BUF/Z（place239/Z），按照lib的定義BUF是不能反向傳遞的，所以，F(xiàn)M-579的影響，到place239這里就截止了（注意到，place239/Z的負(fù)載只有一個(gè)），并不會(huì)影響其他的地方。



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

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

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

審核編輯：劉清