code with function verification failed

signed to unsigned assignment occurs

The code from front_end engineer have some "function module " , there's no warning when I do synthesis with DC, but when I do verification with Formality, this module runs about 6 hours and report Formality meets a fatal error and give up. I tried again,but it happed again!
I checked the netlist and found there's no designware multiplier. Can any one give me some help ?

This is part of the code:
#----------the function------------------------
function [63:0] MUL64xPOW;
input [63:0] V;//
input [6:0] i;//
input [63:0] c;//
reg [63:0] temp0;//
integer cnt;
begin
temp0 = V;
for(cnt = 0; cnt < i; cnt = cnt + 1)
temp0 = MUL64x(temp0 ,c);
MUL64xPOW = temp0;
end
endfunction

#----------the code use uper function---------------
always @ (*)
begin
if(integrity_state == S_CALC_P)
begin
temp = msg ^ eval;
for(i=0; i<64; i=i+1)
begin
if(f9_p == 1'b1)
eval_temp = MUL64xPOW(temp,i,64'h1b);
else
eval_temp = 64'd0;
end
eval_next =0;
for(i=0; i<64; i=i+1)
eval_next = eval_next^ eval_temp;
end
else
begin
temp = { eval[63:17], eval[16:0] ^ length_i };
for(i=0; i<64; i=i+1)
begin
if(f9_q == 1'b1)
eval_temp = MUL64xPOW(temp,i,64'h1b);
else
eval_temp = 64'd0;
end
eval_next =0;
for(i=0; i<64; i=i+1)
eval_next = eval_next^ eval_temp;
end
end



#---------my setting information in Formality---------------------------------------

set hdlin_dwroot /opt/synopsys/synopsys_2007.12_SP5
set hdlin_vhdl_87 true
set hdlin_error_on_mismatch_message false
set verification_set_undriven_signals X
set hdlin_unresolved_modules black_box
set verification_clock_gate_hold_mode low
set hdlin_ignore_parallel_case false
set hdlin_ignore_full_case false
set hdlin_ignore_map_to_operator false

set_svf $source_path/$cur_design.svf

elab-311 case statement

1: First, use for( ; description is not a good coding style;
2: It seems that you are using recursion in the function. This maybe cause the synthesis and FV problem.

site:www.edaboard.com formality set svf

in this design may have loop ,so it will make simulator continue to execute!

signed to unsigned conversion occurs. (ver-318)

First , thank yx.yang and lixpjpljx 's reply.

I check the log file of synthesis but can't found any valuable warning of this module, just like these:
Warning: /home1/hewangfeng/zx280402/EPDCP/integrity_snow3g_uplink.v:636: signed to unsigned conversion occurs. (VER-318)
Warning: /home1/hewangfeng/zx280402/EPDCP/integrity_snow3g_uplink.v:545: signed to unsigned assignment occurs. (VER-318)
Warning: /home1/hewangfeng/zx280402/EPDCP/integrity_snow3g_uplink.v:559: signed to unsigned assignment occurs. (VER-318)
Warning: /home1/hewangfeng/zx280402/EPDCP/integrity_snow3g_uplink.v:359: DEFAULT branch of CASE statement cannot be reached. (ELAB-311)
Warning: /home1/hewangfeng/zx280402/EPDCP/integrity_snow3g_uplink.v:399: DEFAULT branch of CASE statement cannot be reached. (ELAB-311)
;

And report_timing -loops to find the loops, but still no.