Question on "local variable flowing out of ORing of two sequences"

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 )