在线咨询
eetop公众号 创芯大讲堂 创芯人才网
切换到宽版

EETOP 创芯网论坛 (原名:电子顶级开发网)

手机号码,快捷登录

手机号码,快捷登录

找回密码

  登录   注册  

快捷导航
搜帖子
查看: 1602|回复: 1

[求助] 使用Formality对比两版rtl,fail的原因?如何debug?

[复制链接]
发表于 2023-9-5 17:48:44 | 显示全部楼层 |阅读模式

马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。

您需要 登录 才可以下载或查看,没有账号?注册

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赋值。例如:





  1. module wrapper0(
  2. input clk,
  3. input A,
  4. input B,
  5. output [7:0] result);

  6. rtl0 rtl0_1(
  7.     .clk     ( clk    ),
  8.     .in_A   ( A     ),
  9.     .in_B   ( B     ),
  10.     .in_C   ( 1'b0 ),
  11.     .in_D   ( 1'b1 ),
  12.     .result ( result ));
  13. 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问题

十分感谢!




发表于 2023-9-6 10:08:49 | 显示全部楼层
单独分析 logic cone,是reference 和 implement 两边的 match 的 compare point 的logic cone 来比较,两边的cone 相等这对 compare point就相等,全部的 compare point 相等,两个电路就相等。不等一般可能是match或者约束有问题,或者电路就是不同。
您需要登录后才可以回帖 登录 | 注册

本版积分规则

关闭

站长推荐 上一条 /1 下一条

小黑屋| 手机版| 关于我们| 联系我们| 在线咨询| 隐私声明| EETOP 创芯网
( 京ICP备:10050787号 京公网安备:11010502037710 )

GMT+8, 2024-11-6 08:16 , Processed in 0.014255 second(s), 6 queries , Gzip On, Redis On.

eetop公众号 创芯大讲堂 创芯人才网
快速回复 返回顶部 返回列表