System assertions

SystemVerilog
,
1

I want to know $past significance with an example . explain me i am a learner. The below example i am watching but it is not understanding to me.

property system_prop;
  @ (posedge clk) 
      ($rose(req) && $past(!req,1)) |=> 
         ($rose(gnt) && $past(!gnt,1));
endproperty
2

In reply to sai ganesh:

I want to know $past significance with an example . explain me i am a learner. The below example i am watching but it is not understanding to me.

property system_prop;
@ (posedge clk) 
($rose(req) && $past(!req,1)) |=> 
($rose(gnt) && $past(!gnt,1));
endproperty

I am providing to you a page from my SystemVerilog Assertions Handbook, 4th Edition that explains the $past; see http://SystemVerilog.us/dollar_past.pdf
In your example, the**$rose**(req) && $past(!req,1) states that you’re looking for a rose (req), which means that req was 0 in the previous cycle, and is 1 in the current cycle. Your’re also ANDing this withe the $past(!req,1), meaning that in the previous cycle req was a 0. Obviously, this is redundant. All you need is

property system_prop;
  @ (posedge clk) 
      $rose(req) |=> $rose(gnt) ;
endproperty

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

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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
3

In reply to ben@SystemVerilog.us:

And to avoid getting X’s from clock tick 1 (with a $past) I suggest you to delay it by ##1 as in:


property system_prop;
  @ (posedge clk) 
      ##1 $rose(req) |=> $rose(gnt) ;
endproperty

Regards
Srini
www.verifworks.com