formality fail,should I modify the RTL or netlist?

[chc1625]

Hi,all

I'm a newbie about formality. Now I use formality and get a fail. I want to know how to debug and modify the RTL to pass the LEC.
Here is the report:

"1 Failing compare point (1 matched, 0 unmatched):

Ref DFF ref:/WORK/fft/tw_0_c_reg17
Impl DFF0X impl:/WORK/fft/tw_0_c_reg17 "


in the RTL, I define this:

.....
reg signed [17:0] tw_0_c;
wire [35:0] tw0;
.....
always@(posedge sys_clk) begin
if(enable) begin
tw_0_c <= #1 $signed(tw0[35:18]);
end
end


I wonder what might cause the formality fail? Should I modify the RTL or netlist to pass the LEC?
Thanks very much!

 

[lostinxlation]

You can't tell why it fails just by looking at the end flop. THe problem is somewhere in the logic cone contributing to the failing flop or just simply mapping failure.

First, make sure no flops are left unmapped. Post the failure log.

 

[dianin]

Are you giving SVF file as guidance to Formality. This file generated from DC/DCT and DC generates it automatically. If you did not give this file to Formality, then first read this file and set the synopsys_auto_setup variable to true.

 

[rca]

normaly the LEC tool didn't make mistake. But it could
a-you must never modify your RTL code to pass LEC, or you can follow some guideline provide by the LEC tool provider.
b-when it failled you need to analyze the log to check any missing files, library, missing mapping point...
c-you can also do LEC hierarchicaly to find which sub-module failled and reduce the design size to be able to find which rtl code is not correctly synthesis or not correctly LEC.
d-The problem can come from the syntheser or the Logic Equivalent Tool.

 

[chc1625]

Yes, you are right. I have find the reason. I have set a sub-module as blackbox, but forget to set_constant one output signal of it.
Thanks very much!

---------- Post added at 11:26 AM ---------- Previous post was at 11:20 AM ----------

Yes, you are right. I have find the reason. I have set a sub-module as blackbox, but forget to set_constant one output signal of it.
Thanks very much!