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

Hi,
I have a question on the the property definition given in paper " SVA Alternative for Complex Assertions
by Ben Cohen, VHDL Cohen Publishing"


property p_check_msg_BAD2;
 BITS_4 sum;
 bit result;
 ($rose(go), sum=0) |->(
 ((vld[->1], sum=sum+data)[*999999]) or
 ($fell(go)[->1], result=check_sum_simple
 (sum, data)) )
 ##0 result; // line 22
endproperty

ap_check_msg_BAD: assert property(p_check_msg_BAD2);
// ** Error: check_sum.sv(22):
** ERROR: Local variable result
is referenced in an expression
where it does not flow.

I am not clear about the statement “local variable result does not flow out of ORing of two sequences”. Can someone explain what that means.

regards,
-sunil

In reply to puranik.sunil@tcs.com:

The assignment to local variable ‘result’ exists for only one of the sequence instead of both the sequences .

On *((vld[->1], sum=sum+data)[999999])
the [*999999] is not needed and does not make sense because
the sequence_match_item sum=sum+data will only be activated when vld==1.
After that, the left sequence is done.
Consider firing a task from the squence_match_item. Something like the following (untested):


default clocking @(posedge clk);  endclocking
// Needed because of the $sampled
task automatic t_sum(); // data is a module signal
  BITS_4 vsum;
  // wait(vld) // no
  fork
    begin : fork_sum 
        while ($sampled(!vld) begin 
            vsum=$sampled(sum) +$sampled(data);
             @(posedge clk); 
    end  : fork_sum 
    begin : vld_go 
        wait($sampled(vld) || $samled(go));
        am_result: assert(check_sum_simple(vsum, $sampled(data)));
    end :vld_go   
  join
endtask: t_sum
ap_sum: assert property($rose(go) |-> (1, t_sum())); 




Thanks Ben for a detailed reply. I am clear about the concept now.
I have another question - Do the sequences have parameters like parametrized classes or module parameters?

regards,
-sunil puranik

In reply to puranik.sunil@tcs.com:

Sequences are within modules, interfaces, checkers.
Sequences can have arguments that can refer to the parameters.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

In reply to ben@SystemVerilog.us:

Hi Ben ,
Could you please further explain the above comment :

On ((vld[->1], sum=sum+data)[*999999])
the [*999999] is not needed and does not make sense because
the sequence_match_item sum=sum+data will only be activated when vld==1.
After that, the left sequence is done.

‘or’ operator completes as soon as the former of LHS or RHS is true.
Let’s assume a case that $fell(go) is never true .
Won’t local variable sum be assigned on each occurrence of vld[->1] then ?
So the only way ‘or’ operator completes is when the LHS ( vld[->1] ) is true , 999999 times consecutively .
This would mean that sum is assigned 999999 times ( using prior value of sum )

Please correct me if wrong .

Thanks ,
hisingh

In reply to hisingh:
( sequence_expr {, sequence_match_item } ) [ sequence_abbrev ]
1800: Consecutive repetition ( [*const_or_range_expression] ): Consecutive repetition specifies finitely many iterative matches of the operand sequence, with a delay of one clock tick from the end of one match to the beginning of the next. The overall repetition sequence matches at the end of the last iterative match of the operand.

When the sequence_expr is a match the sequence_match_item is executed.
Thus, in (vld[->1], sum=sum+data )[*3]
when vld[->1] is a match (i.e., when the sequence ends with vld==1) the
sum=sum+data is executed. You then repeat that operation 3 times.

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 )

In reply to hisingh:

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 )

Yes.


 (1, sum=sum+1)[*1:99999] ##0 vld; // sum==0 initially
// if vld=1 after 100 cycles, sum==100