Problem with equivalence check (synopsys Formality)

[stevenv07]

Hello,

I have a problem with equivalence check between RTL and gate-level netlist. The problem may be related to error FM-503.
could you help me point out this issue?

Thanks in advance.

Steven

--- Updated Sep 10, 2020 ---

Of course, I already included *.svf file during Formality setup.

 

[stevenv07]

I found that the pipelining with the design-ware multiplier "DW02_mult_6_stage" (Synopsys) causes this problem. I already used .svf file generated by Design Compiler during the Formality verification. However, the error still occurs.

Can anyone help me solve this issue?