formality black-box help

小弟最近初学formality，虽然能够验证简单的设计，但最user-guide中的black-box很好奇，但是却不理解；现有问题如下：
1.需要定义black-box的是只哪些模块，IP or PAD?
2.如何主动的定义一个module为black-box。定义之后要做哪些其他的申明?
3.我理解的black-box是指设计中的一些module只用检查ref和imp的pins，不检查功能，什么时候需要使用black-box。

我的感觉是 很多macro， ip ， pad，psychial only cell都是BB ，
这个FM 跑下就知道了，他们从.lib 里面能自动检测的，

恩，我也是这样认为。但是我在跑一个带有pad的设计时，读入了两个库，分别是pad和core，那么在fm时，是否将pad生成为black-box?还有，如果一般的IP核，我调用的时候，也加入了他IP的库，那么fm会不会生成black-box?
如果芯片厂提供这样的库，那不是black-box就没什么意义了?

reference userguide , you will find the solution！

对 ，看看 user guide
我们的感觉是 读入了 .LIB，里面有些这个模块的功能描述
如果PR 前后对模块不变的话，应该是 FM 不关心的，