In reply to ben@SystemVerilog.us:
Thanks for reply.
I created a waveform to test p until q in the simulation.
p,q is bit signal. clock period is 10
time:0,10,20,30,40,50,60,70,80
p:0, 0, 0, 0, 0, 1, 1, 1,
q:0, 0, 0, 1, 1, 1, 1, 1,
The simulation result:
assertion start at 10 ,fail at 10
assertion start at 20 ,fail at 20
assertion start at 30 ,fail at 30
assertion start at 40 ,success at 40
assertion start at 50 ,success at 50
assertion start at 70 ,success at 70
Question1:
In the spec (434):
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 tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 evaluates to true
It means that p1 must be true at starting clock tick. But,the tool show assertion success at 40,50. At starting clock ticks(40,50), p1 is zero. I don’t know why tool say the assertion success. What is your opinion?
Question2:
In the spec(Page.472) :
An evaluation attempt of a property of the form property_expr1 until property_expr2 is
nonvacuous if, and only if, there is a clock event in which either the evaluation attempt of
property_expr1 or the evaluation attempt of property_expr2 is nonvacuous, property_expr2 does not hold in prior clock events, and property_expr1 holds in all prior clock events.
It seems that there is conflict with page 434. In page 472 mentions that p1 fail and p2 is nonvacuous true. Then, the whole property is nonvacuous true. But, In page 434 it mentions that the whole property is true only when p1 is true and p2 is true. Please correct me if i am wrong.
Thanks a lot!!!