Counting number of events on clock a, while clock o is forbidden

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