Question

SystemVerilog
1

Hi All,

the simulation shows

started at 85ns succeeded at 85ns
started at 95ns succeeded at 95ns

According to spec, an until property of the non-overlapping form evaluates to true if property_expr1 evaluates to true at every
clock tick beginning with the starting clock…
P is zero at 85,95 ns, therefore the property should be failed. Why the result show property passed at 85ns,95ns?
Thanks a lot!

2

In reply to peter:

See
https://verificationacademy.com/forums/systemverilog/simple-assertion-req-implies-ack-does-not-fail

3

In reply to ben@SystemVerilog.us:

Hi Ben,
in my simulation ,B is 1 at 85ns,95ns.
In your table, condition for true Outcome(P2) , P2 is true now(because B is 1 at 85,95ns).
In your table, condition for true Outcome(P1) , when P2 is true, P1 may be false in last cycle.
,so P1 is true now(because A is zero in 85,95ns).
Do you mean that P1 until P2 this property is true only if condition for True outcome(P1) and condition for True outcome(P2), both condition are true?
Please correct me if i am wrong.
Thanks !

4

In reply to peter:

that P1 until P2 this property is true only if condition for True outcome(P1) and condition for True outcome(P2), both condition are true?
Please correct me if i am wrong.

You have P until Q.
Both P and Q are each sequences of 1 term; since they are sequences, theP until Q
have no vacuity issues since neither P or Q can be nonvacuous properties.
Properties that are sequences are never vacuous.
Thus, P1 until P2is true only if P1 is true at all cycles until P2 is true.
In the cycle P2 is true, P1 can be True or can be false.

5

In reply to ben@SystemVerilog.us:

Thanks for reply. Let me confirm again
From 0 to A+1 cycle, P1 is zero,
From 0 to A cycle P2 is zero, A+1 cycle P2 is 1.
So that P1 until P2 is true. Am I correct?

6

In reply to peter:

I can’t follow your a and b.
However, I can say that
A until B // is same as
A[*0:$] ##1 B