SVA: repetition vs delay

property X;
@(posedge clk)
   A ##[1:10] B ##[1:5] C;
endproperty

Does the above go through all 10x5=50 combinations?
I mean A is 1 on cycle 3 and 5, but B is 1 on cycle 10 only. C is always 1.
Simulator:
cycle 1 - A is 0
cycle 2 - A is 0
cycle 3 - A is 1 → checking B, going through cycles 4 to 8, B is never 1 for that time range
cycle 4 - A is 0
cycle 5 - A is 1 → checking B, going through cycle 6 to 10, B is 1 on cycle 10 → checking C → SVA PASSED.

Will the following SVA be treated in a similar way?

property Y;
@(posedge clk)
   (!A)[*0:9] ##0 (!B)[*0:4] ##0 C;
endproperty

Or would it be:
cycle 1 - A is 0
cycle 2 - A is 0
cycle 3 - A is 1 → checking B, going through cycles 4 to 8, B is never 1 for that time range → SVA FAILED.

In reply to Alex K.:

You have multiple threads
A ##[1:10] B ##[1:5] C; // is same as
A ##[1] B ##[1] C or
A ##[1] B ##[2] C or

A ##[1] B ##[5] C or // AND (that is an error)
… with the ##[2], ##[3] up to
A ##[10] B ##[1] C or // AND
A ##[10] B ##[2] C or // AND

A ##[10] B ##[5] C;
You can use the first_match for the search of the first occurrence of a thread.

I STRONGLY suggest that you read my paper Understanding the SVA Engine (item 3 in my signature) if you really want to understand these concepts along with the treads and how they
relate in antecedents and consequents.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: * Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
  1. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

In reply to ben@SystemVerilog.us:

Thank you, Ben!

In reply to ben@SystemVerilog.us:

Hi Ben,
It should be OR instead of AND?

In reply to timag:
Thanks for the correction. My apologies.
I updated my reply.


a1: assert property(@(posedge clk) a ##[1:2] b);
// sequence is same as 
a ##1 b or a ##2 b;