[sv-ac] vacuous evaluation

dratf7 adds  rules for vacuity for new operators. I've doubts on them: 

- "An evaluation attempt of a property of the form always property_expr is
non-vacuous iff if, and only if, there is a clock event where the evaluation
attempt of property_expr is non-vacuous, and property_expr does not fail in
prior clock events."

 Why the sentence about failure is added with rule that fail cannot occure
before nonvacuous evaluation on property expression?

- "An evaluation attempt of a property of the form nexttime property_expr is
non-vacuous iff if, and only if, there is at least one more clock event, and
in the evaluation attempt that start in the next clock event, property_expr
is non-vacuous. "

 From above I think that all nexttime family evaluation is vacuous if there
is no (N) next cycle to check it?

- "An evaluation attempt of a property of the form s_eventually
property_expr is non-vacuous iff if, and only if, there is a clock event in
which the evaluation attempt of property_expr is non-vacuous, and the
property_expr does not hold in prior clock events."

from above one can think that if property expression hold in previous cycles
then the evaluation is vacuous !

 

DANiel

 


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.