请教formality工具的RTL VS RTL的问题，求教~

wuhanouyang

Hello各位大佬，我们项目有个模块A由于需求变化从一个层次结构移到另一个层次结构。但是从顶层看整个模块功能是等效的。
但是在formality工具报的failing point如下，可以看到该rd_ptr_sync_reg[0]寄存器输入均是0，但是输出ref是1，imp是0，patterms窗口如右图，没太看懂这个问题应该如何定位与解决。是不是同一个模块在不同hier下需要手动去匹配上？

                               
登录/注册后可看大图

该寄存器的具体代码如下(ref和imp均使用同一份代码)

wire [3: 0] rd_ptr_sync_nxt ={rd_ptr_sync[2: 0], rd_ptr_sync[3]};
always @(posedgeaclk or negedge aresetn)
  begin : p_rd_ptr_sync
    if (laresetn)
      rd_ptr_sync <= {{3{1'b0}},1'b1};
    else if (rd_ptr_upd_en)
      rd_ptr_sync <=rd_ptr_sync_nxt;
  end

温柔阴影

没 match上，整个模块的flop应该都不能被match，需要手动match

wuhanouyang

温柔阴影 发表于 2024-7-16 14:26
没 match上，整个模块的flop应该都不能被match，需要手动match

set_user_match有办法把整个模块设置成match吗？好像文档里没有提到

温柔阴影

wuhanouyang 发表于 2024-7-16 15:13
set_user_match有办法把整个模块设置成match吗？好像文档里没有提到

应该不行吧。但是report unmatch ，用脚本处理一下应该不难。其实你这个需求应该用跑仿真或者跑sec的方式验证。

kk2009

这种应该用assertion的方式来做等效检查。