|
马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。
您需要 登录 才可以下载或查看,没有账号?注册
x
本帖最后由 伊凡正在学习IC 于 2023-9-6 14:22 编辑
现有两版rtl代码:rtl0和rtl1,rtl1是在rtl0的基础上进行了部分逻辑优化,但模块的整体输出是没有变化的,想用formality对比,以验证两版rtl是否逻辑等价,不要出现非预期的改动。
先说一下design的功能是实现乘、乘加、乘累加等,通过不同inputs信号配置design执行不同功能。
我在多番尝试formality时,由于始终fail,所以就分别在rtl0和rtl1外又包了一层wrapper,让wrapper的inputs只有clk、部分design的inputs信号和计算结果的输出信号,在wrapper内部例化design,并按功能给design的剩余inputs赋值。例如:
- module wrapper0(
- input clk,
- input A,
- input B,
- output [7:0] result);
- rtl0 rtl0_1(
- .clk ( clk ),
- .in_A ( A ),
- .in_B ( B ),
- .in_C ( 1'b0 ),
- .in_D ( 1'b1 ),
- .result ( result ));
- 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问题?
十分感谢!
|
|