In reply to ben@SystemVerilog.us:
After more thoughts, I believe that property is incorrect. Consider this instead
property p_data_unique;
int v_serving_ticket;
@(posedge clk) ($rose(a), v_serving_ticket=ticket, inc_ticket()) |=>
((a [->4]) intersect !o[*] )
##[1:5] $rose(a) && $rose(o)
&& now_serving==v_serving_ticket;
// With the ##[1:$] property will never fail. Suggest adding a limit, such as 5, or 10
endproperty