问下关于formality的问题~~关于verify过程

我用formality验证RTL代码和DC综合出的代码~verify的时候进度从昨天晚上到今天一直卡在95%的进度动不了了~
请教有没有大神遇到过这种情况?是确实卡住了还是可能花的时间比较长，应该多等等?
在redhat的终端里的消息如下：
Status:  Verifying...
start_gui
.............................. 0F/0A/5380P/2613U (67%) 10/13/10 20:44 408MB/1650.74sec
Compare point DIG_LMS_MA/RX_D7_IN_TMP_reg[3] failed (is not equivalent)
Status:  Matching hierarchy...
Status:  Verifying...
.............................. 1F/0A/7614P/378U (95%) 10/13/10 21:15 408MB/2608.68sec
.............................. 1F/0A/7614P/378U (95%) 10/13/10 21:46 408MB/3300.01sec
.............................. 1F/0A/7614P/378U (95%) 10/13/10 22:25 477MB/4254.46sec
.............................. 1F/0A/7614P/378U (95%) 10/13/10 22:55 477MB/5009.25sec
.............................. 1F/0A/7614P/378U (95%) 10/13/10 23:31 477MB/5873.21sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 00:10 477MB/6848.16sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 00:50 477MB/7794.67sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 01:20 477MB/8579.74sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 01:51 477MB/9340.43sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 02:22 477MB/10080.96sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 02:56 477MB/10918.87sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 03:27 477MB/11645.91sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 03:57 477MB/12381.43sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 04:27 477MB/13108.33sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 04:58 477MB/13846.07sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 05:28 477MB/14589.53sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 05:59 477MB/15358.99sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 06:29 477MB/16031.21sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 06:59 477MB/16769.99sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 07:30 477MB/17508.39sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 08:00 477MB/18244.59sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 08:30 477MB/18984.52sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 09:01 477MB/19725.86sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 09:31 477MB/20472.40sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 10:02 477MB/21160.09sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 10:33 477MB/21725.48sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 11:09 477MB/22222.61sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 11:39 477MB/22762.69sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 12:10 477MB/23467.76sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 12:40 539MB/24195.75sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 13:13 539MB/24969.34sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 13:49 539MB/25837.30sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 14:24 539MB/26709.10sec
.............................. 1F/0A/7614P/378U (95%) 10/14/10 14:54 539MB/27472.52sec

没碰到这种情况，你换个版本试试。

没有见到过

我遇到过,总是在98%的时候死在那里,后来是拿到ICC中心去跑的,跑过了,我们的服务器太差

我用cadence的conformal LEC遇到过这样的问题，通常由于比较规模太大或者内存不够造成的。解决办法：
1.   检查是否用的64bit操作
2.  能否化为hierarchy 的方法比较
3.  增加内存，或者增加swap的大小

有时候还和match结果相关的，我以前也遇到过，你把match的结果贴出来看看

确实没有遇到过

用LEC试过在95%卡了很久，但最后还是能跑过的

遇到过，有时候是有些点有bug，的确是会一直卡在那里。
你最好在脚本中设不会运行好久，出置运行时间，一般formality出现这种情况肯定是因为有些点formality无法验证，在脚本中设置时间不要运行太久，然后再rpt中看unvarified的报告，看看哪些无法验证，这样比较好查问题。

检查设计中是否存在组合Loop，
还有，将综合产生.svf文件读入fm，有利于fm验证效率。

擦，原来是1年前的帖子，被翻出来了，晕菜~