浅析Formality形式验证里的案件

在当前的形式验证的领域，主要有两个工具，一个就是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误动作。

审核编辑：刘清