LEC的几个问题

1.使用formality做LEC需要用到.svf文件具体是做什么的?
2.对应使用conformal做LEC不需要吃这种文件吗?
3.confomal吃进的udp.v是做什么用的?
4.如果设置一个macro为blackbox，那么是不是就不用吃他们的library了?
求大神解决

没用过C家的，说一下FM:
1.SVF就是记录了DC compile时的一些操作，比如replace,merge,constant reg,retiming等。尤其是syn 时做retime的话，不带SVF一般不会过fm。FM可以吐出可读的svf,可以看到具体内容。
4.FM里有set_black_box可以对cell/design设black box. 但是memory/macro之类的,就算你读了db, FM也看不到内部逻辑的,没法比较内部,所以一般都会当做black box啊.
所以,有db就给,FM会当做black box;没有也可以不给,link不上,可以把hdlin_unresolved_modules设black_box.

谢谢！

4.如果不吃blackbox 的library，那么他们的端口处是怎么处理的?

bbox input pin 当做logic cone的outputbbox output pin 当做logic cone的input