A simple assertion; req implies ack; does not fail

SystemVerilog
, , ,
8

In reply to timag:
A notation in my table:
1 (yellow bold)== nonvacuous true in a clocking event;
1 (plain text)==hold (vacuous or nonvacuous)

From 1800 page 472 "An evaluation attempt of a property of the form property_expr1 until property_expr2 is nonvacuous if, and only if,

  1. there is a clock event in which either the evaluation attempt of property_expr1 or the evaluation attempt of property_expr2 is nonvacuous,
  2. property_expr2 does not hold in prior clock events,
  3. and property_expr1 holds in all prior clock events."

Q1:Do you mean case1 and case2 pass and case 3 fail?

From my table:
Conditions for nonvacuity and true outcome
p1 until p2,
case1:
p1: 11110
p2: 00001

case2:
p1: 11111
p2: 00001

case3:
p1: 11110
p2: 00001

If I want P2 only response p1, it means that p2 can not be 1 unless p1 is active.
How should I do?

So you are asking for the case where the nonvacuous true for the until applies when any attempt of P1 is nonvacuous and P2 is also nonvacuous. Is that the question?
The way it is defined in 1800, for a nonvacuous true then P1 can be vacuous at all attempts so long as p2 is nonvacuous.
To get what you want restrict your properties to sequences since the
evaluation of sequences as properties cannot be vacuous.