讨论：Formality和后仿真，为什么会一个对，一个错！！！

orinoflow

大家好，我的设计，在DC综合之后做后仿真和Formality，Formality是通过了，报告附在后面（大家也帮我判断下，报告如下，是不是真的算通过了）。但是否仿真一个Case的时候就出错了，我通过仿真波形跟踪到一个memory的写入逻辑，差了一拍，因为跟踪波形太痛苦，没有继续跟下去。DC报告中时序是正常的，没有问题(有0.02的setup的violation，但是我留了4ns的余量)。我现在感觉疑惑的是，什么情况下会导致Formality正确而后仿真不正确呢？有没有大侠有这方面的经验？
我在论坛上看到过这样一个帖子，讨论同样的问题 ，但是没有最终结果，大家可以参考：
http://bbs.eetop.cn/viewthread.php?tid=240374&page=1


以下为我Formality的结果

* Matching 结果如下：*
9883 Compare points matched by name   
1823 Compare points matched by signature analysis   
0 Compare points matched by topology   
356 Matched primary inputs, black-box outputs   
427(2083) Unmatched reference(implementation) compare points   
0(0) Unmatched reference(implementation) primary inputs, black-box outputs   
1749(33) Unmatched reference(implementation) unread points   
----------------------------------------------------------------------------------------   
Unmatched Objects                                                        REF        IMPL   
----------------------------------------------------------------------------------------   
Black-boxes (BBox)                                                        0           2   
Registers                                                               427        2083   
   DFF                                                                    45           0   
   Transparent LAT                                                         8           0   
   Clock-gate LAT                                                          0        2083   
   Constrained 0X                                                        347           0   
   Constrained 1X                                                         27           0   
****************************************************************************************


# Verification 结果如下：
Verification SUCCEEDED
   ATTENTION: RTL interpretation messages were produced during link
              of reference design.
              Verification results may disagree with a logic simulator.
-----------------------------------------------------------------------
Reference design: r:/WORK/XDPTOP
Implementation design: i:/WORK/XDPTOP
11706 Passing compare points
----------------------------------------------------------------------------------------
Matched Compare Points     BBPin    Loop   BBNet     Cut    Port     DFF     LAT   TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent)         559       0      51       0      55   11036       5   11706
Failing (not equivalent)       0       0       0       0       0       0       0       0
Not Compared
  Unread                       4       0       0       0       0     497       0     501
****************************************************************************************

zh123456789

这是有可能的啊。fm这个东西我看未必靠得住啊，大小的设计都会报告有很多not compared的地方，那么verify的结果也不大可信吧。

orinoflow

怎么看具体哪些点没有被Compare呢？

heguo1983@hot

呵呵这种现象太正常了

liushutao

很可能是时序的问题
fm只验证功能不保证时序，如果时序有问题，fm过了方针也不对的。

rencj1979

楼上的正解，保证时序应该run sta吧，formality又不能保证时序

guozhujun1

学习了，谢谢！

yhang0

formality只是对比逻辑功能而已，不保证时序的

q4949

FM 过，Post sim 不过很正常
1. 一定要找到错误点,不要偷懒.
2. 查是不是有时序约束的例外：多周期约束或者false path.
3. 是不是hold 问题？
4. 是不是仿真模型导致的错误？