A problem when using $past() for systemverilog assertion

caowangyang · November 6, 2015, 1:56pm

Hi, Dear,

Recently I am writing an assertion which would be used to check the behavior of a counter - SAMPCNT :

SAMPCNT will be inside 0 ~ 255.
Once the counter toggled, it will counter down from 255 to 0, previous SAMPCNT always be larger than current SAMPCNT.
Once the RESETSAMP asserted, the SAMPCNT will be reset to 255.

So what I write is that :


dpc_sampcnt_behavior_check : assert property ( @(SAMPCNT) (!$isunknown(SAMPCNT)) |-> 
                                               ( SAMPCNT >= 0 && SAMPCNT <= 255 ) && 
                                               ( $past(SAMPCNT) > SAMPCNT || ( $past(SAMPCNT) < SAMPCNT && SAMPCNT == 255 && RESETSAMP ) ) ) 
                                                 $display("SAMPCNT = [0x%0h]'d%0d, past(SAMPCNT) = [0x%0h]'d%0d, RESETSAMP = %0d", SAMPCNT, SAMPCNT, $past(SAMPCNT), $past(SAMPCNT), RESETSAMP);
                             else $error( $psprintf("ERROR RESETSAMP = %0d, SAMPCNT = [0x%0h]'d%0d, past(SAMPCNT) = [0x%0h]'d%0d", RESETSAMP, SAMPCNT, SAMPCNT, $past(SAMPCNT), $past(SAMPCNT)) );

However, I got assertion error as :

ncsim: *E,ASRTST (interface/counter_if.sv,718): (time 4815958196171 FS) Assertion tb_top.if_counter[0].dpc_sampcnt_behavior_check has failed
ERROR RESETSAMP = 0, SAMPCNT = [0xfd]'d253, past(SAMPCNT) = [0x6]'d6 → ERROR Message
SAMPCNT = [0xfc]'d252, past(SAMPCNT) = [0xff]'d255, RESETSAMP = 0 → DISPLAY Message

When I looked at waveform, I just found that the SAMPCNT behave as :

8 → 6 → 255 → 253 → 252 → 250 …

I have two questions :

Why the display message and error message is different for $past(SAMPCNT) ? The display message is what I expected …
When $past(SAMPCNT) = 6, I definitely expect SAMPCNT = 255, but how can it jump directly to 253 and skip 255 ? In which case, my assertion failed.

I am really thanking for your great help, I need support here, thanks ! thanks ! thanks !

caowangyang · November 6, 2015, 5:00pm

In reply to ben@SystemVerilog.us:

There are several things that just don’t look correct:

the clocking event You use @(SAMPCNT), but that is not a clocking event. If anything it is a vector (SAMPCNT will be inside 0 ~ 255).
even if a signal, called “a”, doing the following is meaningless:

a_ : assert property(@(a)  a);  
// If posedge(a) , then (a) is sampled just before the posedge, i.e., (a)==0
// If negedge(a), then (a) is sampled just before the negedge, i.e., (a)==1
The @(a) means that the clocking event for the assertion is at both edges

The values used for all design variables inside the expressions of an assertion are those sampled at the Preponed region. However, the $sampledis necessary in an action block, which does not follow/utilize the sampled semantics and hence uses the current values of the variables at the time the action block is evaluated. For example;

apCounterMaxed : assert property ( @ (posedge clk)
disable iff (!reset_n) go |=> (cntr <= 3)) else $error("%0t SVA_ERR: Counter exceeded 3, cntr %0d; sampled(cntr) %0d ", $time, cntr, $sampled(cntr) ); // Application of $sampled

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
Component Design by Example ", 2001 ISBN 0-9705394-0-1
VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

Hi, Ben,

Thanks so much for your great help, the @(SAMPCNT) is indeed not a clock event, but seems it could work in my case, because I want this assertion could work whenever SAMPCNT changed. So that is why I used @(SAMPCNT), is it ok ? Since I didn’t find an alternative clocking event here.

Your second note is very help, I planed to use $sampled() function for every variable of assertion as a try, on the other side, could you please teach me where I could learn more for the knowledge of “simulation timing region” ? I am really confused for this topic always.

Thanks again, thanks so much :-)

Best Regards,

WangYang

ben2 · November 6, 2015, 8:29pm

In reply to caowangyang:

…the @(SAMPCNT) is indeed not a clock event, but seems it could work in my case, because I want this assertion could work whenever SAMPCNT changed

NO, that is not correct.
The @(SAMPCNT) is really fired if SAMPCNT, which is between 0 and 255 (per your requirements), changes from anything other than 0 to 0, or from 0 to anything other than 0. However, going from 5 to 6 is not an event. Also, study my point 2 in my previous response. Doesn’t your counter have a clock? What decrements the counter? a clock?
Without doing detailed analysis of your assertion, this is most likely what you want. You need to check your requirements:

… whenever SAMPCNT changed

$stable returns true if the sampled value of the expression did not change between the sampled value at the previous cycle and the sampled value at the current cycle. Otherwise, it returns false. $changed is a complement to $stable; $changed returns true if the sampled value of the expression changed. Otherwise, it returns false.

[Ben] You should write smaller assertions; they are easier to follow.

// 
let a = SAMPCNT;  // easier for me to type for now. 
// SAMPCNT will be inside 0 ~ 255.
default disable iff !rst_n;
default clocking cb_clk @ (posedge clk); endclocking
a_inside255 : assert property(@(posedge clk) a >=0 && a <255 );   **// <--- UPDATED**

// Once the counter toggled, it will counter down from 255 to 0, previous SAMPCNT always be larger than current SAMPCNT
a_inc  : assert property($changed(a) |-> $past(a) > a );   // using the default clocking 

// Once the RESETSAMP asserted, the SAMPCNT will be reset to 255.
a_resetcntr : assert property(RESETSAMP |-> a==255);

could you please teach me where I could learn more for the knowledge of “simulation timing region” ?

I previously posted a copy of the section of my SVA book that addresses timing regions at

Timing regions are also in the 1800-21012 LRM

Ben SystemVerilog.us

caowangyang · November 7, 2015, 3:55am

In reply to ben@SystemVerilog.us:

Hi, Ben,

Thanks again for your great information.

I still have question on @(SAMPCNT). I didn’t get your point there. In Verilog LRM, @(SAMPCNT) will be explained by “any value changed”, so why I can’t use this expression here to indicate whenever the SAMPCNT changed, is there any side-effect ?

Since I am new to SVA, so thanks for your patience :-)

WangYang

ben2 · November 7, 2015, 5:07am

In reply to caowangyang:

My mistake on how the @count vector works; you’re correct in that, but I rarely use the @ of a vector. However, you need to understand the difference between sampled and current value. Consider the following example

module atcount; 
	bit clk, a; 
	bit[2:0] count; 
	default clocking @(posedge clk); endclocking
    initial forever #10 clk=!clk;  
    always_ff @ (posedge clk)  
      count <= count+1'b1; 
     
    always @ (count) begin
       $display("current count=%b, sampled count=%b", count, $sampled(count));
    end 
endmodule : atcount

Simulation produced the following results:

run 100ns
# current count=001, sampled count=000
# current count=010, sampled count=001
# current count=011, sampled count=010
# current count=100, sampled count=011
# current count=101, sampled count=100

When you do


assert property ( @(SAMPCNT) (!$isunknown(SAMPCNT)) |-> 
                                               ( SAMPCNT >= 0 && SAMPCNT <= 255 )
// The !$isunknown(SAMPCNT), SAMPCNT >= 0 , etc is NOT the current value of SAMPCNT, but the sammpled value of SAMPCNT.  Thus, you need to understand the following 
a_ : assert property(@(a)  a);  
// If posedge(a) , then (a) is sampled just before the posedge, i.e., (a)==0
// If negedge(a), then (a) is sampled just before the negedge, i.e., (a)==1
The @(a) means that the clocking event for the assertion is at both edges

In any case, it is not correct to use the @(signal) as the clocking event.
If you want to create your own reality, vision, or doctorate paper on this issue, please be my guest. However, this is NOT how SVA is used. In fact, most users prefer small assertions, and the clocking event is the clock edge that produces the change.

BTW, I updated

a_inside255 : assert property(@(posedge clk) a >=0 && a <255 );   **// <--- UPDATED**

Ben SystemVerilog.us

caowangyang · November 10, 2015, 9:30am

In reply to ben@SystemVerilog.us:

Hi, Ben,

Thanks so much for your detailed information.

Last quick question : After we used @(posedge clk) as clock even for an assertion as following, the value inside the expression will still be sampled value just before the posedge clock, is that right ?

a_inside255 : assert property (@(posedge clk) a >= 0 && a < 255);

The “a” is always refer to the value before the posedge clk, is that right ? Namely, sampled value in Preponed Region ?

Thanks,

WangYang

Srini · November 10, 2015, 9:58am

In reply to caowangyang:

In reply to ben@SystemVerilog.us:
Hi, Ben,
Thanks so much for your detailed information.
Last quick question : After we used @(posedge clk) as clock even for an assertion as following, the value inside the expression will still be sampled value just before the posedge clock, is that right ?

a_inside255 : assert property (@(posedge clk) a >= 0 && a < 255);

The “a” is always refer to the value before the posedge clk, is that right ? Namely, sampled value in Preponed Region ?
Thanks,
WangYang

Yes, “a” shall be the sampled value from preponed region.

Srini

caowangyang · November 11, 2015, 5:58am

In reply to Srini @ CVCblr.com:

Hi, Srini,

Got it, Thanks.