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

In reply to Jadoon:


//in my previous code with the TB I have 
 // Let k==5
  ap_AsFrom: assert property(@(posedge clk)  		                            
      (($rose(rst) ##1 a[->4]) intersect !o[*]) ##1 a[->1] |-> 
                                                    o==1'b1 ##1 a ~^ o[*1000]); 
And that worked. By now you got the needed cpncepts.  Test my code.