How assumptions work in formal tool

In reply to ashish_banga:


 if signal is one clock cycle wide .  it should toggle only once. 
 it requires some support logic. 
 bit set_a_flag ;
function void set_flag(bit a_flag);
       set_a_flag = a_flag ;
endfunction  

property a_toggle_once ;
@(posedge clk)
 (a==0 ,set_a_flag==0,set_flag(1))|-> ##1 (a==1)[->1] #1 a ==0 ;
endproperty