Formality 验证lowpower syn deisgn时到底要不要把UPF load 进来

金角大王G

如题，想问下FM 大神，Syn 阶段load_upf 后插了lowpower cell;
请问下在比FM （RTL2PRE_NETLIST）的时候，到底需不需要load UPF 并将verification_force_upf_supplies_on 设为OFF， 让FM 去推所有的OFF2ON 情况？

我这边个人认为是没必要的， 即如果load UPF 了，也只需要check all ON 状态；不load UPF 直接比FM 应该也需要能过；
如果FM 有能力比power OFF2ON 等相应的feature ，那么CLP 存在的意义也就没了~

欢迎讨论~~~

gushenglin

点赞，一起求解

金角大王G

来来来，顶一个呀，畅所欲言，讨论讨论嘞~~~

zero_0

这不仅仅是supply的问题呀，不吃UPF的话isolation signal的存在就已经改变function了

金角大王G

zero_0 发表于 2024-8-6 18:29
这不仅仅是supply的问题呀，不吃UPF的话isolation signal的存在就已经改变function了 ...

所以把ISO_EN set_constant 到0 ，跟RTL 保持一致

金角大王G

zero_0 发表于 2024-8-6 18:29
这不仅仅是supply的问题呀，不吃UPF的话isolation signal的存在就已经改变function了 ...

那你load upf 的时候，不会撞到tool 把你Supply 的state 撞到1，然后输出就是X 了？

zero_0

X没问题呀，只要X=0和X=1都等价就可以了

金角大王G

zero_0 发表于 2024-8-7 09:58
X没问题呀，只要X=0和X=1都等价就可以了

欸，我这遇到的： RTL/PRE_NET 都load_upf;
但是ref , FM 识别的pg_info，以ISO 为例，从GUI 来看，它只识别一个power_info，就我UPF 里面 -isolation_power_net 指定的；
但是Imple 中，对已经存在的那个PISO， 它会有VDD(primary_power0/VDDO(backup_power)/VSS(ground), 这三者组合DC 就是1，导致输出X ，R/I就不match 了~


以下均以Implement 中要给ISO 为例：（我也不明白它列的是dont_care ，但按后面的表达式输出就是X）

                               
登录/注册后可看大图

                               
登录/注册后可看大图

                               
登录/注册后可看大图

aaronqi

我在AMD做了9年formality检查，对于低功耗设计，绝对有必要load upf，将supply on的参数disable后做等价性检查。CLP检查不能代替power aware 的Formal 检查。

金角大王G

aaronqi 发表于 2024-8-7 21:02
我在AMD做了9年formality检查，对于低功耗设计，绝对有必要load upf，将supply on的参数disable后做等价性 ...

哎呦我去~~~
OKOK，那请问下如果load UPF 之后不等基本上由什么引起？ 我这边load UPF 后不等，基本上都是由下面这种造成的，我还真不知道怎么解，
会撞到REF 中ISO 出一个值，但是IMPLE 中由于power 的状态造成X

                               
登录/注册后可看大图