within Operator

The within operator is used to express the containment of a sequence within another sequence.

Syntax:

<seq_exp> within <seq_exp>

The construct seq1 within seq2 is an abbreviation for

[1[*0:$] ##1 seq1 ##1 q[*0:$]] intersect seq2

The “seq1 within seq2” matches for a finite interval of consecutive clock ticks if seq2 matches along with the complete interval and seq1 matches for sub-interval of consecutive clock tick and must satisfy the below conditions

The start point of the match of seq1 must be greater than or equal to the start point of the match of seq2.
The endpoint of the match of seq1 must be less than or equal to the endpoint of the match of seq2.

within operator example

valid [*5] within (($rose req) ##1 req[*6])

Explanation

When valid is low consecutively for 5 cycles within req goes high and followed by 1 clock cycle req signal stays high for 6 cycles. The above sequence matches if req remains set for 6 clock cycles and valid is set for 5 consecutive clock cycles within the same window.

not Operator in an assertion

The not operator is used to express the non-occurrence of the sequence.

Syntax:

not (<seq_exp>);

not operator example

sequence seq;
  req1 ## valid;
endsequence

property prop;
  @(posedge clk) !en |-> (not (seq));
endproperty

assert property prop;