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

Status
Not open for further replies.

chc1625

Newbie level 4
Joined
Aug 28, 2010
Messages
5
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,281
Activity points
1,318
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
 
Last edited:

I don't remember the command, but yes, mapping commands exist in every formal verification tools. Check the manual.
 
set_user_match rathin ref iath in implemention
 
I have fixed the problem. The reason is I forgot to read some svf file of the sub-module.
 

Status
Not open for further replies.
Cookies are required to use this site. You must accept them to continue using the site. Learn more…