Equivalent expression for intersect operator

SystemVerilog
, , , ,
1

Hi Moderators,

For an ‘intersect’ operator to succeed the lhs & rhs sequence must be of the same length

(a) Both lhs & rhs sequence must match at the starting clock

(b) Both lhs & rhs sequence must end at the same clock

Consider the following concurrent assertion

a1:assert property( @(posedge clk) seq_exp[*1:$] intersect $rose(sig)[->1] );

(Q1) I wanted to confirm if the following is the equivalent expression for a1 ? ::

( seq_exp[*1] intersect $rose(sig)[->1] ) or
( seq_exp[*2] intersect $rose(sig)[->1] ) or
( seq_exp[*3] intersect $rose(sig)[->1] ) or
.........................................
( seq_exp[*N] intersect $rose(sig)[->1] ) or

(Q2) Would a1 pass, as soon as the intersect operator succeeds for any of the sub-sequence ?

Thanks

2

I’ve really enjoyed thinking carefully about this question (and have enjoyed the introduction to the intersect operator).

Reading through carefully, I think the answer is probably “yes” to both Q1 and Q2, except for the fact that I suddenly realised I’m not sure about how to match seq_exp[*1:$]. Working from IEEE 1800-2017, I find the following text:

- Consecutive repetition ( [*const_or_range_expression] ): Consecutive repetition specifies finitely
  many iterative matches of the operand sequence, with a delay of one clock tick from the end of one
  match to the beginning of the next. The overall repetition sequence matches at the end of the last
  iterative match of the operand. [*] is an equivalent representation of [*0:$] and [+] is an
  equivalent representation of [*1:$].

I assume that “the last iterative match of the operand” doesn’t require the operand to stop matching afterwords. (So I’d expect it to be possible to match 1 [*] before the end of a simulation), but I couldn’t convince myself of this. I’d love to hear from someone knowledgeable.

Assuming I did guess correctly, I think I agree with the equivalence. Indeed, I think that these two sequences are equivalent:

  (seq1 or seq2) intersect seq3

  (seq1 intersect seq3) or (seq2 intersect seq3)

and the proposed equivalence in Q1 is just doing that repeatedly (an unbounded number of times!)

Incidentally, the fact that you’re using a property means that it can be written with until as well. I think this is probably equivalent:

  a2: assert property (@(posedge clk) seq_exp ##1 (seq_exp until_with $rose(sig))