A problem when using $past() for systemverilog assertion

SystemVerilog
, , ,
2

In reply to ben@SystemVerilog.us:

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

  1. 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).
  2. 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