讨论：Formality和后仿真，为什么会一个对，一个错！
时间：10-02
整理：3721RD
点击：
大家好，我的设计，在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 ObjectsREFIMPL
----------------------------------------------------------------------------------------
Black-boxes (BBox)02
Registers4272083
DFF450
Transparent LAT80
Clock-gate LAT02083
Constrained 0X3470
Constrained 1X270
****************************************************************************************
# 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 PointsBBPinLoopBBNetCutPortDFFLATTOTAL
----------------------------------------------------------------------------------------
Passing (equivalent)55905105511036511706
Failing (not equivalent)00000000
Not Compared
Unread400004970501
****************************************************************************************
我在论坛上看到过这样一个帖子，讨论同样的问题 ，但是没有最终结果，大家可以参考：
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 ObjectsREFIMPL
----------------------------------------------------------------------------------------
Black-boxes (BBox)02
Registers4272083
DFF450
Transparent LAT80
Clock-gate LAT02083
Constrained 0X3470
Constrained 1X270
****************************************************************************************
# 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 PointsBBPinLoopBBNetCutPortDFFLATTOTAL
----------------------------------------------------------------------------------------
Passing (equivalent)55905105511036511706
Failing (not equivalent)00000000
Not Compared
Unread400004970501
****************************************************************************************
这是有可能的啊。fm这个东西我看未必靠得住啊，大小的设计都会报告有很多not compared的地方，那么verify的结果也不大可信吧。
怎么看具体哪些点没有被Compare呢?
呵呵这种现象太正常了
很可能是时序的问题
fm只验证功能不保证时序，如果时序有问题，fm过了方针也不对的。
楼上的正解，保证时序应该run sta吧，formality又不能保证时序
学习了，谢谢！
formality只是对比逻辑功能而已，不保证时序的
FM 过，Post sim 不过很正常
1. 一定要找到错误点,不要偷懒.
2. 查是不是有时序约束的例外：多周期约束或者false path.
3. 是不是hold 问题?
4. 是不是仿真模型导致的错误?