[sv-ec] Concurrent assert statement within procedural block

Hi,

I have a query regarding concurrent assertions statement :

sequence s1;
 @ (posedge clk) (counter1 == 3) ##3 (counter1 == 4);
endsequence

property p1;
  (counter1 == 13) ##[0:4] (counter2 == 3) ##1 (counter1 == 15);
endproperty

property p2;
  @ (posedge clk) p1;
endproperty

always @ (posedge clk)
begin
  my_assert1 : assert property (s1);
              
  my_assert2 : assert property (p2);
              
end

Since  the property can be asserted inside a procedural block, is the 
property evaluated sequentially?
Or is the behaviour same as if it was asserted outside the always block ?
Does both property evaluation start at the posedge of clk simultaneously?

Regards,
Sarani



-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.