formality的不确定性

最近用了下formality，这个工具让我很头大，居然DC综合后的都过不了，检查发现是如下这个句子：
$signed(a)+$signed(b)+$signed(c) > $signed(4'b0011) ?1:0;
这种语句好像他们的解释不太一致，问题是我相信谁呢?仿真我看不到错误，上面的句子如果把前面三个相加改为两个，没问题。或者把这三个数相加从新用个变量把结果算好，再放则个式子也没问题，，
真不懂，这样的软件居然还敢拿出来卖，当然，这个句子lec也通过不啦哈哈，看来天下的算法都差不多，，我感觉太绝望了。

盼望高手解答

同样更诡异的是，我加了clock gating后，设置了验证模式，然后验证通不过，但仔细看pattern里面，好像又是对的，电路图也是。我怀疑formality认为是ref里面的时钟为高就要判断，而实际上应该是网表里面寄存器的时钟端为高才检查嘛，要不设置验证模式有什么用呢?
是不是有什么地方可以设置哦，只有在门控后的时钟为高才检查而不是rtl的时钟?

有没有相关的应用手册哦，目前只有user guiad是根本不够用的

综合后过不了，你读入svf了吗?
工具有bug也是正常的，如果工具做出来直接完美，那还是人做的东西吗?
你怎么敢这么自信不是你自己的问题而是工具有问题?Synopsys成堆的
工程师，又是业界标准，吹出来的吗?
fm过不了多想想自己是不是有问题，别张嘴就喷工具怎么怎么样。

一看这小子就没有亲自做过，呵呵

“上面的句子如果把前面三个相加改为两个，没问题。或者把这三个数相加从新用个变量把结果算好，再放则个式子也没问题”
我根据这个猜测是读取SVF，指定TOP，这个过程有问题。我曾经遇过相似的问题，就是我刚才说的问题。report_svf 看看有没有与此电路相关的。

都找到原因了还说什么啊。
复杂了工具认不出来正常，下次就就遵守规则写fm认得出的code 就好

fm确实让人很头大，加入clk gating和dft之后，layout前后同版的netlist一般可以过，但是相同的rtl DC综合出不同版的netlist我试了几次，基本跑不过，不过本人正在学习熟悉这个东西，应该是有些东西还没掌握