Advanced Sequence Operators

Matches when two sequences start at the same time AND end at the same time.

// Check that 'burst_write' sequence happens exactly during 'enable_window'
sequence s_burst;
    req ##1 ack ##1 data[*4]; // Length = 6
endsequence
property p_intersect;
    @(posedge clk) start_burst |-> (s_burst intersect enable_window);
endproperty
                            

• Requirement: Length(Seq1) must equal Length(Seq2).
• Use Case: Verifying that a packet transfer completes precisely before a timer expires.

Matches if Sequence 1 starts after or with Sequence 2, and ends before or with Sequence 2. S1 is "contained" inside S2.

// 'ack' must arrive somewhere inside the 'request' window
property p_within;
    @(posedge clk) req |-> (ack within (req ##[1:100] done));
endproperty
                            

This is looser than intersect. S2 acts as a container/envelope.

Checks that a boolean expression (signal) remains TRUE for the entire duration of a sequence.

// 'reset' must remain LOW throughout the entire burst transfer
property p_no_reset_during_burst;
    @(posedge clk) start_burst |-> (!reset_n) throughout (req ##1 ack ##1 data[*4]);
endproperty