Hi All ,
I was trying following code to note differences between sequence methods .matched and .triggered :: edaplayground
The property expression ::
@( posedge clk ) $rose( c ) |=> @( posedge clk ) aRb(a,b).matched / aRb(a,b).triggered
is Equivalent to :: @( posedge clk ) $rose( c ) |=> aRb(a,b).matched / aRb(a,b).triggered !!
In both cases the $display within the sequence executes at T:45 however ::
(1) Via +define+TRIGGER :: The assertion Passes at T:45
(2) Via +define+MATCH :: The assertion FAILS at T:45
Both methods .matched as well as .triggered are True in Observed Region so why is it that the assertion fails for +define+MATCH ?
LRM 16.13.6 says ::
"The value of method triggered evaluates to true (1'b1) if the operand sequence has reached its end point at that particular point in time and false (1'b0) otherwise. The triggered status of the sequence is set in the Observed region and persists through the remainder of the time step."
"Unlike triggered, matched provides synchronization between two clocks by storing the result of the source sequence until the arrival of the first clock tick of the destination sequence after the match. The matched status of the sequence is set in the Observed region and persists until the Observed region following the arrival of the first clock tick of the destination sequence after the match."
Although destination and source clock are the same i.e @( posedge clk ) , it seems that .matched still waits for Next clock edge for the assertion to PASS
i.e if I were to write ::
property endCycle ;
`ifdef MATCH
@( posedge clk ) $rose( c ) |=> ##1 aRb(a,b).matched ;
...........
endproperty
The assertion PASSes at TIME: 55 although the $display from sequence executes at TIME:45