In reply to ben@SystemVerilog.us:
Seems I got the answer, using two assertions:
$rose(rst) |=> (a[->4] intersect !o[*]) ##1 a[->1] ##0 o==1'b1;
$rose(rst) |=> o[->1] ##0 a==1'b1 ##1 a ~^ o[*1000];
First assertion forbids O for 4 events of A, followed by 5th A with O.
Second assertion checks for O and expects A that time. It is to catch the violation:
rst…a…a…a…a…o…a
It is followed by the XNOR pattern. Just one question, I tried this assertion with the range a ~^ o[*1:$] and it didn’t worked. Can you refer to some detailed reading material for the reason behind it?
thanks a ton.