formality问题请教

雨打溪风

在做形式验证中有一个命令如下：

set verification_set_undriven_signals 0:X

这句命令的具体含义是什么？
user guide中的解释是：treats undriven pins and nets in the reference design as "0", and those in the implementation design as "X" 。该怎么解释？？

为什么加了这个设置命令之后，一些原先Verify fail的最后都pass 了？

tomzhuo

不知道

lca6

不知道

fu2006

set verification_set_undriven_signals 0:X
设计中有些没有连接的pins，若其没有驱动的话，formal工具在比较时，由于逻辑锥的起点未驱动，可能会出现fail，ref为1/0,im为0/1； 加上了如上的语句之后，会把该未驱动的pins在逻辑锥的起点上在ref时，force成0，而impl上force成X，则X代表了此时不会去做比较。故可以pass吧。