Ben,
On testing the code from above pdf
bit clk , a = 1 , b ;
always #5 clk = !clk;
property p;
realtime v;
int count;
($fell(a), v=$realtime, count=0) |-> @(clk) ( ($changed(b), count++)[*1:$] intersect a[->1] )
##0 @(posedge clk) $realtime - v == 20ns ##0 count==20;
endproperty
ap:assert property( @(posedge clk) p);
initial begin
#14; a = 0; // Antecedent matches at T:15 & consequent starts evaluation
#06; b = !b; // T: 20 'b' toggles for the 1st time
// Assume that 'b' toggles 19 more times before 'a' is asserted
#2 $finish();
end
Assertion fails at T:15 as lhs of intersect is false whereas rhs matches due to !a[*1]
( RHS a[->1] is equivalent to !a[$0:$] ##1 a )
For intersect to pass both lhs & rhs should match at T:15 i.e the starting clocking event
I believe property ‘p’ is incorrect since it expects $changed(b) to match on every clocking event i.e @(clk)
Since this thread already has a lot of replies I am thinking to create a new one to discuss possible solution using concurrent assertion.
Will share the link here once I post it
EDIT :: using-go-to-v-s-non-consecutive-repetition-within-intersect-operator