In reply to ben@SystemVerilog.us:
Thanks Ben .
So when vld[->1] is true for 2nd time , the previous value of sum ( assigned when vld[->1] was true for 1st time ) is used to calculate the new value of sum.
So had we written :
property p_check_msg_BAD2;
BITS_4 sum;
bit result;
($rose(go), sum=0) |-> (
( ( vld[->1], sum=sum+data )[*3] ) or ( $fell(go)[->1] , sum = sum+data ) )
##0 ( 1 , result = check_sum_simple(sum, data) ) ##0 result;
endproperty
Assuming that $fell(go) is never true , the ‘or’ operator is true only when vld[->1] is true thrice ( sum is assigned thrice as well )