Multiple UVM info at same posed cause false increment as a result of which the assertion fails

[NimishaV]

Hello, I have written the following property to check that the actual valid count (ie the number of times wr_vld is high) is less that or equal to the expected valid count calculated from vld_count, the valid is counted as long as I have wr_vld high and until I see an instr_done or clr ==1 where it reset the counter to 0. However, the assertion works fine under some cases but for few tests, the uvm_info gets displayed twice in the same cycle leading to incrementing the counter twice in one cycle as a result of which the actual count exceeds the expected count but in reality from the waveform it is less that the expected value. It is basically due to multiple uvm_info in same cycle. The error message is also shown below. What could be the reason for it?The arrow (|) points at until in the property. Please help!

Also, is there a way I can increment the count in the property itself instead in the function and just display the counter values in the function for the following implementation? I tried one way to increment the counter in the property but it increment only once. Also tried to include [*0:$] to increment on every clock as long as the valid is high but even that didn’t work!

function int wr_num_exp_instr(int calc_vld_count);begin
begin wr_num_exp_instr = calc_vld_count;end
uvm_info("PROPERTY",$psprintf(" EXPECTED INSTRUCTION COUNT :%0d",wr_num_exp_instr) ,UVM_NONE) end endfunction function int wr_act_instr_cnt_func( int wr_exp_instr_cnt);begin if(instr_done ==1 || clr == 1) wr_act_instr_cnt_func = 0; else wr_act_instr_cnt_func++; line 514 uvm_info(“PROPERTY”,psprintf("label ACTUAL VALID COUNT IS :%0d label EXPECTED INSTRUCTION COUNT:%0d ",wr_act_instr_cnt_func,wr_exp_instr_cnt) ,UVM_NONE) end endfunction property wr_num_instr_match_num_vld_start_p; int wr_exp_instr_cnt; int wr_act_instr_cnt ; @(posedge clk) disable iff(!rstn || disable_check == 1) (((enable==1) ##0 first_match( ##[0:] drm_wr_vld) |-> (((wr_vld,wr_exp_instr_cnt = wr_num_exp_instr(vld_count),wr_act_instr_cnt = wr_act_instr_cnt_func( wr_exp_instr_cnt)) |-> (wr_act_instr_cnt<=wr_exp_instr_cnt)) until (instr_done,wr_act_instr_cnt =wr_act_instr_cnt_func(wr_exp_instr_cnt))) ;
endproperty
assert property (wr_num_instr_match_num_vld_start_p)
else begin
`uvm_error(“PROPERTY”,$psprintf("wr_num_instr_match_num_vld_start_p failure "))
end;

UVM_INFO sva_cov.sv(532) @ 97000: reporter [PROPERTY] EXPECTED INSTRUCTION COUNT :14
UVM_INFO sva_cov.sv(514) @ 98000: reporter [PROPERTY] label ACTUAL VALID COUNT IS :14 label EXPECTED INSTRUCTION COUNT:14
UVM_INFO sva_cov.sv(514) @ 98000: reporter [PROPERTY] label ACTUAL VALID COUNT IS :15 label EXPECTED INSTRUCTION COUNT:14
(((enable==1) ##0 first_match( ##[0:$] drm_wr_vld) |-> (((wr_vld,wr_exp_instr_cnt = wr_num_exp_instr(vld_count),wr_act_instr_cnt = wr_act_instr_cnt_func( wr_exp_instr_cnt)) |-> (wr_act_instr_cnt<=wr_exp_instr_cnt)) until (instr_done,wr_act_instr_cnt =wr_act_instr_cnt_func(wr_exp_instr_cnt))) ;
|
xmsim: *E,ASRTST (sva_cov.sv,517): (time 98 NS) Assertion sva.wr_num_instr_match_num_vld_start_p has failed (1 cycles, starting 98 NS)
UVM_ERROR sva_cov.sv(525) @ 98000: reporter [PROPERTY] wr_num_instr_match_num_vld_start_p failure

[ben2]

In reply to Nimisha Varadkar:
It is difficult for me to debug this unless I get the total picture, such a an assertion testbench. In any case, I do have some pointers and things I noticed about your style.

1. functions should be automatic, particularly for assertions
2. Functions should not have side effects, unless they affect the testbench environment, such as support logic.
3. Overuse of unnecessary begin … end. DO this instead

function automatic int wr_num_exp_instr(int calc_vld_count);
wr_num_exp_instr = calc_vld_count;
`uvm_info("PROPERTY",$psprintf(" EXPECTED INSTRUCTION COUNT :%0d",wr_num_exp_instr) ,UVM_NONE)
endfunction

4. I fail to understand the wr_act_instr_cnt_func++;
   You mean else wr_act_instr_cnt_func= wr_act_instr_cnt+1’b1; ??

function automatic int wr_act_instr_cnt_func( int wr_exp_instr_cnt);
if(instr_done ==1 || clr == 1) wr_act_instr_cnt_func = 0;
else wr_act_instr_cnt_func++;  // <<< ??? WHAT IS THIS???
`uvm_info("PROPERTY",$psprintf("label ACTUAL VALID COUNT IS :%0d label EXPECTED INSTRUCTION COUNT:%0d ",
wr_act_instr_cnt_func,wr_exp_instr_cnt) ,UVM_NONE)
endfunction
// *** A better way ??
function automatic int wr_act_instr_cnt_func( int wr_exp_instr_cnt, wr_act_instr_cnt);
if(instr_done ==1 || clr == 1) wr_act_instr_cnt_func = 0;
else wr_act_instr_cnt_func= wr_act_instr_cnt+1'b1;  // <<< <------------
`uvm_info("PROPERTY",$psprintf("label ACTUAL VALID COUNT IS :%0d label EXPECTED INSTRUCTION COUNT:%0d ",
wr_act_instr_cnt_func,wr_exp_instr_cnt) ,UVM_NONE)
endfunction

5. I don’t care for the use of multiple implication operators. DO you really mean vacuity in the 2nd antecendent?

(((enable==1) ##0 first_match( ##[0:$] drm_wr_vld) |->
(((wr_vld, wr_exp_instr_cnt = wr_num_exp_instr(vld_count),
wr_act_instr_cnt = wr_act_instr_cnt_func( wr_exp_instr_cnt)) |->
(wr_act_instr_cnt<=wr_exp_instr_cnt)) until (instr_done,wr_act_instr_cnt =wr_act_instr_cnt_func(wr_exp_instr_cnt))) ;

I understand that the until operator is for a property, and that is why you use the |->. However, you can have a sequence followed by a property with the #-# operator. If you want to stick to sequences, you can use the throughout operator. Thus,

// use this instead
property wr_num_instr_match_num_vld_start_p;
int wr_exp_instr_cnt;
int wr_act_instr_cnt ;
@(posedge clk) disable iff(!rstn || disable_check == 1)
(((enable==1) ##0 first_match( ##[0:$] drm_wr_vld) |->
(((wr_vld, wr_exp_instr_cnt = wr_num_exp_instr(vld_count),
wr_act_instr_cnt = wr_act_instr_cnt_func( wr_exp_instr_cnt, wr_act_instr_cnt)) #-#
(wr_act_instr_cnt<=wr_exp_instr_cnt)) until
(instr_done,wr_act_instr_cnt =wr_act_instr_cnt_func(wr_exp_instr_cnt, wr_act_instr_cnt))) ;

6. Again, those are general comments. In any case, the assertion should be passive, and can only make changes to the testbench environment, the support logic.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
   Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
3. Papers:

• SVA Alternative for Complex Assertions
  Verification Horizons - March 2018 Issue | Verification Academy
• SVA in a UVM Class-based Environment
  SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
• Understanding the SVA Engine,
  Verification Horizons - July 2020 | Verification Academy

[NimishaV]

In reply to ben@SystemVerilog.us:

1. if I use automatic it creates separate thread and increment only once the value remains 1 for all incrementation.

2. The begin and end is used for `uvm_info or else it shows error.
   4.yes, that it what I meant.

3. No the logic is working fine, the incrementation also occur as desired except for the few cases in which someone the function gets called twice and which increments the count more than required.
   6.yes, take care of that

Are throughout and until functionally the same? How will be the implementation with throughout?

[ben2]

In reply to Nimisha Varadkar:

In reply to ben@SystemVerilog.us:

1. if I use automatic it creates separate thread and increment only once the value remains 1 for all incrementation.

• Sorry, I don’t get your original point from the title “Multiple UVM info at same posed cause false increment”. UVM_INFO is a display message.
• At every clocking event an assertion thread is started. Any increment performed in a function called within a sequence_match_item should be automatic. A function can be void or it can return a single value. Thus, if you have 2 values to return to property local variables you must write two separate functions; I made a mistake in my response. Below is an example.

function automatic int fnv1(int v1, bit d);
if(d) fnv1=v1+1'b1; else fnv1=v1;
`uvm_info("PROPERTY",$psprintf(" EXPECTED INSTRUCTION COUNT :%0d",fnv1) ,UVM_NONE)
endfunction
function automatic int fnv2(int v2, bit d);
if(d) fnv2=v2-1'b1; else fnv2=v2;
endfunction
property p_test;
int v1, v2;
($rose(a), v1=1, v2=3) |-> ##2 (c, v1=fnv1(v1, d), v2=fnv2(v2, d));
endproperty
ap: assert property(@ (posedge clk) p_test );   

3. The begin and end is used for `uvm_info or else it shows error.

OK

4.yes, that it what I meant.

see my first response on using functions to update local variables.

5. No the logic is working fine, the incrementation also occur as desired except for the few cases in which someone the function gets called twice and which increments the count more than required.

Your code has too many errors. Fix it first. I don’t see the case of the calling twice if a function returns a single value that is assigned to a local variable.

Are throughout and until functionally the same? How will be the implementation with throughout?

   property_expr1 until property_expr2 -- the until is property operator 
   
   $rose(req) |=> busy until ready); //   Identical to
   $rose(req) |=> busy[*0:$] ##1 ready ; // equivalent property expression
   // busy can be 1 or 0 when ready==1

   EXP throughout SEQ   //  sequence operator 
   // The throughout operator is used to check for a Boolean condition 
   // to be true during a sequence.
     sequence R; $fell(c) ##1 d[->1]; endsequence 
     ap1: assert property(@ (posedge clk) $rose(a) |-> b throughout R);  
     // is equivalent to $rose(a) |-> b [*0:$] intersect R 
     //  When d==1 b==1  -- unlike the until 
     ap2: assert property(@ (posedge clk) $rose(a) |-> ##[1:3] b ##1 c throughout d [->1]); 
        // the throughout acts like an until_with 
        // c throughout d [->1])  equivalent to 
        // c until_with d 

I hope that this clarifies things a bit.
Ben SystemVerilog.us