Assertion for a signal until a sequence is triggered

SystemVerilog
1

Hi all, how to model this requirement using assertion?

Once Seq 1 is triggered(Antecedent), signal b should remain constant until Seq 2 is triggered

2

property P1;
@(posedge clk)
seq1.triggered |-> ($stable(signb) throughout seq2.triggered);
endproperty

3

Hi @flyant , i think it will fail always because once the antecedent is matched, it will just check that seq2 has reached it’s endpoint or not in the same cycle (as you have used |-> ), if not then assertion will fail. It will not check the actual intended behavior that until seq2 is triggered, signal b should remain stable.

4

I will double check with throughout, I remember if we use the sequence here, it will wait until seq2 is triggered.

but you can try this way instead.
property P1;
@(posedge clk)
seq1.triggered |-> ($stable(signb) throughout seq2.triggered[->1]);
endproperty

1 Like
5

Yes, this will work. But i am not sure that if it is legal to use goto operator with sequence. Let me try.

6

Thanks @flyant . It’s working. GOTO operator is illegal when we use with sequence but as we’re using triggered method for the sequence which returns a Boolean value, so it can be used.

7

You may be interested in my
SVA paper: (intersect) vs (throughout, until, until_with, within) *** MUST READ FOR REAL SVA USERS!!! *** It addresses misunderstandings in the use of these operators, often caused by inherent misconceptions arising from their English-like syntax. https://lnkd.in/g5sREUuk