求助，如何做synthesis netlist vs post_route netlist的验证

如题
目前我使用formality，做过dc netlist vs rtl的验证。但是题目中的验证怎么做?
还有一个问题
我们的设计没有加入decap filler。但是合作方要求加decap，但又要求不能加太多，只加在core的四周。encounter中的加add decap filler命令是什么?如何控制加在core的四周?以及选用什么size的filler 比较好?

形式验证的流程是一样的啊，还比rtl vs netlist快很多。
encouter 没用过，icc 中可以将decap 当作std filler 加将去，要加在某一区域可以用坐标范围控制。

decap为什么要加在core四周呢?
根据decap的作用，我觉得分散开来，然后在时钟树附近加一点 比较好吧。

1.做形式验证不一个模式的吗 就是两个输入的netlist 不一样而已
该等同的等同 该ignore的ignore 不过没用过formality
你这题目的两个netlist 应该比你做的简单啊
2.
addDeCap
[-help]
-totCap capacitance
[-cells cellName ...]
[-addFixAttr]
[-area llx lly urx ury]
[-exclude {llx lly urx ury} ...]
[-effort [low | high]]
[-prefix prefixName]
[-noFixDRC]
[-force]
[-log ecoFile]
[-fromFile ecoFile]
[-powerDomain powerDomainName]
[-pgNet netName]
命令是有的吗 你可以自己写个perl 或者 tcl 来处理这样的情况

runLEC check by Conformal

恩，知道是这个形式验证的流程
但是遇到了一些问题
做dc net与postroute net时，我发现有很多unmatch的cell，这些cell都是我设计中存在的，比如与门或者其他什么门?
还有个问题：svf文件是我在做rtl vs dc net时用的，现在做dc net vs postroute net时还需要么?

svf 不需要了吧。可以先看看寄存器是不是全都对上了。如果都对上了，再看看那些没对上的 cell 是否是DECAP这种可以忽略的。