浅析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误动作。
比亚迪与佛山塑胶集团合资扩建锂离子电池隔膜项
如何解决教育机器人刚需问题，让教育机器人走的更长远呢？
解答真空断路器为什么过电压及防范措施
如何使用Python爬虫抓取手机APP的数据
针对车辆通讯协议一致性测试的电动汽车充电桩模拟器
浅析Formality形式验证里的案件
苹果美国官网开售官翻版iPhone 11系列
集成电路替换技巧
碳化硅功率器件的封装—三大主流技术
微雪电子7寸电容触摸彩色LCD显示模块简介
双电层电容器的工作原理和特点
基于FPGA芯片为核心实现通用实验系统的软硬件设计
哪些牌子的蓝牙耳机性价比高？双十二值得购买的四款蓝牙耳机
好用的开发工具平台推荐
诺基亚8发布最新消息:前后同拍创意十足! 良心保留3.5mm耳机接口,诺基亚8王者归来
区块链为什么是个好市场
高效节能的物联网加密技术
农业无人机的六大用途是什么
苹果手机将在2019年之后增加睡眠追踪功能
如何让站点式远程监控系统的数据传输问题变得简单化
通常情况下，形式验证的工具的主战场，是在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误动作。
比亚迪与佛山塑胶集团合资扩建锂离子电池隔膜项
如何解决教育机器人刚需问题，让教育机器人走的更长远呢？
解答真空断路器为什么过电压及防范措施
如何使用Python爬虫抓取手机APP的数据
针对车辆通讯协议一致性测试的电动汽车充电桩模拟器
浅析Formality形式验证里的案件
苹果美国官网开售官翻版iPhone 11系列
集成电路替换技巧
碳化硅功率器件的封装—三大主流技术
微雪电子7寸电容触摸彩色LCD显示模块简介
双电层电容器的工作原理和特点
基于FPGA芯片为核心实现通用实验系统的软硬件设计
哪些牌子的蓝牙耳机性价比高？双十二值得购买的四款蓝牙耳机
好用的开发工具平台推荐
诺基亚8发布最新消息:前后同拍创意十足! 良心保留3.5mm耳机接口,诺基亚8王者归来
区块链为什么是个好市场
高效节能的物联网加密技术
农业无人机的六大用途是什么
苹果手机将在2019年之后增加睡眠追踪功能
如何让站点式远程监控系统的数据传输问题变得简单化