disable iff
In certain design conditions, we don’t want to proceed with the check if some condition is true. this can be achieved by using disable iff.
Below property checks that, if the signal “a” is high on given posedge of the clock, the signal “b” should be high for 3 clock cycles followed by “c” should be high after ”b” is high for the third time. During this entire sequence, if reset is detected high at any point, the checker will stop.
property p; @(posedge clk) disable iff (reset) a |-> ##1 b[->3] ##1 c; endproperty a: assert property(p);
ended
while concatenating the sequences, the ending point of the sequence can be used as a synchronization point.
This is expressed by attaching the keyword “ended” to a sequence name.
sequence seq_1; (a && b) ##1 c; endsequence sequence seq_2; d ##[4:6] e; endsequence property p; @(posedge clk) seq_1.ended |-> ##2 seq_2.ended; endpeoperty a: assert property(p);
Above property checks that, sequence seq_1 and SEQ_2 match with a delay of 2 clock cycles in between them. the end point of the sequences does the synchronization.