[sv-ac]16.14.8 Nonvacuous evaluations accept/reject // Do need your feedback

I need clarification on vacuity for the accept_on/reject_on family of abort
operators. Some internal discussions with people in the industry believe
that the vacuity definition as it currently stands is incorrect. Currently
the LRM basically says that *accept_on*(*condition*) is nonvacuous if *
condition *is true, and *reject_on*(*condition*) nonvacuous if *condition *is
true. The vacuity definitions would be hard to change now, as we're in
draft 4 of the revised 1800-2012 document and changes are very hard to do
now. However, regardless of that, I believe that there will be objections
to make the aborts nonvacuous when the abort *condition *is true. This is
because the *accept_on/reject_on *are abort properties. If an abort
property gets aborted as nonvacuous then it means that it was a true
pass/fail in simulation. However, when an abort property is vacuous, it
can still contribute to the evaluation of a complex property where the
outcome is nonvacuous.
On a personal basis, I see this vacuity of the abort property confusing to
the user. Consider for example the following:
ap_xfr_accept: *assert property* (
    (*$rose*(req) |-> (*first_match* (##[1:5] ack)) #-#
       (*sync_accept_on*(cancel) transfer_envelope[*256])) or
       (interrupt [->1])
    );

  ap_xfr_reject: *assert property* (
    (*$rose*(req) |-> (*first_match* (##[1:5] ack)) #-#
       (*sync_reject_on*(cancel) transfer_envelope[*256])) or
       (interrupt [->1])
    );

* For the case of *ap_xfr_accept *the assertion passes vacuously if *
cancel==1 *before an *interrupt*.
* For the case of *ap_xfr_reject *a *cancel==1 *requires* an interrupt *for
the assertion to pass*. *

 I would like to hear your comments.
Thanks,
Ben Cohen SystemVerilog.us

> ---------- Forwarded message ----------
>> From: Ben Cohen <hdlcohen@gmail.com>
>> Date: Mon, Feb 6, 2012 at 4:14 PM
>> Subject: Re: [sv-ac]16.14.8 Nonvacuous evaluations // question on
>> accept/reject forms
>> To: sv-ac@eda-stds.org, "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
>>
>>
>> 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_exp**r *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> 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> 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
>>>>
>>>
>>>
>>
>>
>

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