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

SystemVerilog
, ,
19

In reply to ben@SystemVerilog.us:

I tried the property:
(($rose(rst) ##1 a[->4]) intersect !o[*]) ##1 a[->1] |-> o==1’b1 ##1 a ~^ o[*1000]);

but it fails for the case when 2 events of A have occurred and then O comes (but with no A). It doesn’t detect this violation as needed by !o[*] part. Let me simulate further and then will post the image.