Need assistance in understanding an assertion

SystemVerilog
,
1

I am trying to understand the assertion failure for the below property but I am not sure how to analyze since assertion can be triggered either by clock or data

property stat_check;
@(data or posedge clk) disable iff (rst)))
    not ($changed(clk) within (1'b1 ##1 $changed(data) ##1 1'b1));
endproperty

Here is the list of questions:

  1. does ##1 refer to clock or data here?
  2. doesn’t $changed(clk) always return 0 if clk is the reference
  3. Please explain the working of this assertion as I could not find any similar reference with multiple trigger events
2

In reply to vshankr:

your assertion does not make sense. Also, your statement ince assertion can be triggered either by clock or data is false. An assertion triggers at every clocking event.
What are your requirements?
I suggest you read my paper (link below) Understanding the SVA Engine

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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:
3

In reply to ben@SystemVerilog.us:

It’s an assertion generated by CDC tool to verify data is quasi-static.
I tried to make sense of it but I don’t understand fully.

How do we read below statement with reference to assertion:

@(data or posedge clk) disable iff (rst)))

I thought assertion starts new evaluation either when data changes or on posedge of clock. Then again, does ##1 always refer to clk(not data)?

Thanks Ben for the recommendation.

4

In reply to vshankr:
This is a very confusing assertion because
@(data or posedge clk) says that the clocking event that starts the asn is either a change in data or a posedge of clk. There are 2 problems with this:

  • the sampling event for the rest of the assertion is either of 2 events.
    I never used this because the property takes different meanings depending upon which initial clocking event starts the assertion.
  • If data changes from 4’b1001 to 4’b1101 there is no event

I suggest that the assertion be rewritten based on the requirements.

Perhaps the author was trying to say something like


// Guessing here at to the meaning 
// there should never be a clk within 3 cycles consisting of a change of data in cycle 2
 not ($changed(clk) within (1'b1 ##1 $changed(data) ##1 1'b1));
// This is not the way to write it. Yes a ##1 is a 1 clocking event tick. 
// Also, does ##1 does not always refer to clk(not data) in this case, it depends as to what 
// the "initial clocking event ", the one that starts the assertion is.   
// In this model, it could be the @(data) 
// I never saw this type ( @(a) or (b)) of modeling for the clocking event

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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: