formality 顶层验证方法

诸位大侠，描述如下：1、顶层包括几个子模块，子模块分别形式验证通过
2、验证顶层，读入子模块ddc，验证非常慢，需要一周
3、目前需要较快debug，等不了读入ddc的验证了，需要把子模块设置为black box
4、问题是，设置这个black box的标准流程是如何的?我设置hdlin_unresolved_modules black_box 出现BB的不匹配。
求各位大侠指教，谢谢

能否给每个子模块设置建立一个lib，类似于模拟ip之类的lib，这时就不需要考虑每个子模块的匹配了，此时只需要比较模块之间的接口了?
没试过层次化的形式验证，不知道可行不?

哇哦哇哦哇哦