RE: [sv-ac]16.14.8 Nonvacuous evaluations // question on accept/reject forms

Hi Ben,

There is no counting of non-vacuous failures of an assertion, but of all failures, both vacuous and non-vacuous.

Regards,
Dmitry

From: Ben Cohen [mailto:hdlcohen@gmail.com]
Sent: Tuesday, February 07, 2012 02:14
To: sv-ac@eda-stds.org; Korchemny, Dmitry
Subject: Re: [sv-ac]16.14.8 Nonvacuous evaluations // question on accept/reject forms

Sorry to bring this up again, as I have one more question:
LRM says "For an evaluation of reject_on (expression_or_dist) property_expr and of
sync_reject_on (expression_or_dist) property_expr, there is an evaluation of the underlying
property_expr. If during the evaluation, the abort condition becomes true, then the overall evaluation of the
property results in false.

But on vacuity, LRM says "ac) An evaluation attempt of a property of the form reject_on(expression_or_dist) property_expr is
nonvacuous if, and only if, the underlying evaluation attempt of property_expr is nonvacuous and
expression_or_dist does not hold in any timestep of that evaluation attempt."

[Ben] So based on vacuity, an evaluation of reject_on (expression_or_dist) property_expr would be vacuous if during the evaluation of the property_expr the expression_or_dist is true. In that case, when you have an abort condition, I presume that the pass/fail count should NOT be incremented, and if a simulator increments those counters (for the accept_on or reject_on), then that simulator would be in error. I need to confirm this with this committee.

attached is a test case.
Ben

On Mon, Feb 6, 2012 at 3:54 PM, Ben Cohen <hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>> wrote:
OK, my error, the accept is an abort and the result is vacuously true per 16.12.14 Abort properties
"For an evaluation of accept_on (expression_or_dist) property_expr and of sync_accept_on (expression_or_dist) property_expr, there is an evaluation of the underlying property_expr. If during the evaluation, the abort condition becomes true, then the overall evaluation of the property results in true. "
Ben Cohen

On Mon, Feb 6, 2012 at 3:31 PM, Ben Cohen <hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>> wrote:
LRM states: "An evaluation attempt of a property of the form accept_on(expression_or_dist) property_expr is
nonvacuous if, and only if, the underlying evaluation attempt of property_expr is nonvacuous and
expression_or_dist does not hold in any time step of that evaluation attempt."

But in reality, there is another condition where the evaluation attempt of a property of the form accept_on(expression_or_dist) property_expr is
nonvacuous: Specifically if expression_or_dist holds in any time step of that evaluation attempt, then the evaluation is nonvacuous true.
Did we miss that case?

I have similar comments on the other properties with accept/reject

Ben Cohen

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

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