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.
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?
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.
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 )
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.
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 )
