Asynchronous Assertions

I think the below sva code suffice your requirement. Let me if this meets your criteria.


property seq_check;
@(posedge clk);
A1 |-> A1 [*1:$] ##1 (A2 && A1) [*1:$] ##1 (A3 && A2 && A1) [*1:$];
endproperty

assert property(seq_check);


//You may as well use $rose(A1) before the implication operator.