Why i do get this error from SVA: "Property operator usage is not allowed in sequence context. Implication used in sequence context"

Hi There,

I am trying to check if seq1 is being done within seq2 so i wrote my assertion as following:

sequence seq1;
fell(a) |-> ##[1:] $rose(b);
endsequence

sequence seq2;
rose(a) |-> ##[1:] $rose(c);
endsequence

property xyz;
@(posedge clk);
seq1 within seq2;
endproperty

assert property (xyz);

unfortunately i am getting a compiler issue: Property operator usage is not allowed in sequence context. Implication used in sequence context.

so do anyone has any idea why i am getting this compile error?
Thanks in advanced…

In reply to noha shaarawy:

Hi There,
I am trying to check if seq1 is being done within seq2 so i wrote my assertion as following:
sequence seq1;
fell(a) |-> ##[1:] $rose(b);
endsequence
sequence seq2;
rose(a) |-> ##[1:] $rose(c);
endsequence
property xyz;
@(posedge clk);
seq1 within seq2;
endproperty
assert property (xyz);
unfortunately i am getting a compiler issue: Property operator usage is not allowed in sequence context. Implication used in sequence context.
so do anyone has any idea why i am getting this compile error?
Thanks in advanced…

I think you cannot use the implication operator in sequences only in properties. According to the LRM 16.12.7 Implication
The implication construct specifies that the checking of a property is performed conditionally on the match of a sequential antecedent (see Syntax 16-17).
So you need to change your sequences to match the desired behaviour, also keep in mind that having multiple implications in a property can lead to false success (vacuous?).

HTH,
Ronald

Thanks Ronald for the clarification…