使用Formality对比两版rtl，fail的原因？如何debug？

伊凡正在学习IC

现有两版rtl代码：rtl0和rtl1，rtl1是在rtl0的基础上进行了部分逻辑优化，但模块的整体输出是没有变化的，想用formality对比，以验证两版rtl是否逻辑等价，不要出现非预期的改动。

先说一下design的功能是实现乘、乘加、乘累加等，通过不同inputs信号配置design执行不同功能。

我在多番尝试formality时，由于始终fail，所以就分别在rtl0和rtl1外又包了一层wrapper，让wrapper的inputs只有clk、部分design的inputs信号和计算结果的输出信号，在wrapper内部例化design，并按功能给design的剩余inputs赋值。例如：

1. module wrapper0(
   
2. input clk,
   
3. input A,
   
4. input B,
   
5. output [7:0] result);
   
6. 
   
7. rtl0 rtl0_1(
   
8.     .clk     ( clk    ),
   
9.     .in_A   ( A     ),
   
10.     .in_B   ( B     ),
    
11.     .in_C   ( 1'b0 ),
    
12.     .in_D   ( 1'b1 ),
    
13.     .result ( result ));
    
14. endmodule
    

复制代码

wrapper1也如上，只是内部例化了rtl1。
这样写的原因是经过多次formal尝试，如果把rtl的in_C或in_D放在wrapper的端口上，formal就会fail。
但是如果按照上面代码中这样写，formal只在在{in_C,in_D}=2‘b00时fail，赋值为2'b01~2'b11时均能通过。

对此我产生了一些疑惑：

问题1：我查到formality分析设计时，会将reg、black box的输入等作为compare point，将电路划分为logic cone，通过分析logic cone来对比compare point，以证明ref和impl是否等价。
我想知道分析logic cone时，是以它为单独的一个模块分析还是和电路中与它相连的其它logic cone有关？
如果是单独分析logic cone，那我理解应该是不管design的inputs配置成什么值，这段logic cone都会被单独遍历自己的输入以对比输出，为什么我在给design配置不同输入值时，有些能通过formal呢？

问题2：在我令design的{in_C,in_D}=2’b00时，通过debug追到是在一个OV信号=0时，ref和impl的某段logic cone compare fail，但在该配置下，OV信号应该始终为1。如果design的inputs的配置会影响tool分析后面的logic cone的话，这个OV信号就不该出现0的情况。

基于以上问题，想请教各位formality究竟是如何分析logic cone的，design的inputs信号又是如何影响formality分析的？以及在debug时，追到某段logic cone的primary input的值与design当前的inputs配置不符时，应该怎样继续debug问题？

十分感谢！

温柔阴影

单独分析 logic cone，是reference 和 implement 两边的 match 的 compare point 的logic cone 来比较，两边的cone 相等这对 compare point就相等，全部的 compare point 相等，两个电路就相等。不等一般可能是match或者约束有问题，或者电路就是不同。