Formality Check Fails When Checking DesignWare

[zzt001]

checking formality

I need to use Formality to verify a module using DesignWare DW_div_pipe.
Source code in my RTL like the following.

parameter TC = 0 ; // unsigned
parameter REM = 1 ; // remainder
parameter STAGES = 4'd10 ; // total stage
parameter STALL = 1 ; // stallable
parameter RESET = 1 ; // async reset
parameter AU_BDIV_PARA = 'd64 ;

DW_div_pipe #(AU_BDIV_PARA, AU_BDIV_PARA, TC, REM, STAGES, STALL, RESET)
u01 ( .a(diva), .b(divb),
.quotient(divp),
.remainder(divr),
.divide_by_0(div0),
.en(w_en),
.clk(clk),
.rst_n(rstn));
......
But the Formality check result fails. Following is the report.
20 Failing compare points (20 matched, 0 unmatched):

Ref DFF r:/WORK/au_wrap/au_top_inst/u_bigdiv/u01/a_int_reg[2][48]
Impl DFF i:/WORK/au_wrap/au_top_inst/u_bigdiv/u01/U_DIV/au_top_inst_u_b
igdiv_u01_link402026_r_REG530_S2

Ref DFF r:/WORK/au_wrap/au_top_inst/u_bigdiv/u01/a_int_reg[3][52]
Impl DFF i:/WORK/au_wrap/au_top_inst/u_bigdiv/u01/U_DIV/au_top_inst_u_b
igdiv_u01_link402026_r_REG1324_S1
......
I have read in the svf file generated in synthesis procedure. Why it fails? Is there any special config in Formality to check designware like DW_div_pipe? How can I do?
Many thanks for your help.

 

[avimit]

formality designware

Looks like an svf annotation problem.
1. What version of formality are you using.
if you are using the latest then you will see a report in the log file like this:
*****Guidance Summary*******
which will tell you how good your svf annotation was. Look what is rejected and what is accepted.
2. If you are not using latest, i.e you cannot see the above line in your formality run, then,
use the following, after you have done your matching:

report_svf_operation [find_svf_operation -status rejected]

Kr,
Avi
http://www.vlsiip.com
you may want to have a look at
http://www.vlsiip.com/formality

 

[rsrinivas]

report_svf_operation

use
set compile_seqmap_propogate_constants true
may be ur constants are removed during synthesis.

Regards