形式验证的blackbox设置问题

conformal对模块A进行形式验证，现在A顶层是比不过的有abort点，所以选择在底层进行验证，其中子模块B单独验证通过的。
现在在顶层A进行验证的话，想把B设置为blackbox，发现个问题，就是代码文件中的module B在综合过程忠例化了两次，在网表体现了两次分别是B_0,B_1,两个module。
set non_translation B(B_0 B_1） -both之后验证发现blackbox之间的不匹配
G : B
R : B_1
R : B_0
请问该怎么设置才能使他们匹配起来呢?

同求解