Hi Ben,
thanks a lot for detailed reply. Referring to the discussion above on series “aaa” my question was that if there assertion,
a1: assert property (@(posedge clk) a[*1:$] |-> p)
then for example, for input pattern aa in first two clocks, p has to be true in both the clocks for assertion to be true, for pattern aaa, p has to be true in all three clocks, for pattern aaaa, p has to be true in all 4 clocks… etc. Same holds for all n till end of simulation. so does it mean
a1: assert property (@(posedge clk) a[*1:$] |-> p)
is same as
a1: assert property (@(posedge clk) a |-> p)
In the discussion above,
ap3ab: assert property(a[*1:3] ##1 b |-> p);
ap3abfm: assert property(first_match(a[*1:3] ##1 b) |-> p);
both these assertions are not same due to first_match. For ap3ab to succeed, all the threads in attempt need to succeed while in ap3abfm, one you get one match, assertion succeeds and others threads need not succeed. Is that correct?
Also if the assertion a1 is in initial block, it will start only one attempt at first clock. Is this understanding correct?
rgs,
-sunil