How to tell formality to match two points with different name?

[chc1625]

Hi,all

In the rtl, I define a two-dimension array like this: reg [15:0] ibuf0_rd[11:0]; . After dc synthesis, the register are changed name to ibuf0_rd_reg1511,ibuf0_rd_reg1510.... so the formality can not match the ibuf0_rd_reg[15][11] in ref and ibuf0_rd_reg1511 in netlist,
are there some command tell formality match them?

Thanks

 

[lostinxlation]

I don't remember the command, but yes, mapping commands exist in every formal verification tools. Check the manual.

 

[sachin_kirdat]

set_user_match rathin ref iath in implemention

 

[chc1625]

I have fixed the problem. The reason is I forgot to read some svf file of the sub-module.