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:
does ##1 refer to clock or data here?
doesn’t $changed(clk) always return 0 if clk is the reference
Please explain the working of this assertion as I could not find any similar reference with multiple trigger events
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
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