RE: [sv-ac] Notes of false vacuity + NO Meeting on Tuesday

Hi Ben,

As far as I remember, there is no counting of negative vacuous attempts in the LRM defined. We can, of course, discuss it during the work on the next PAR. Note, however, that we should distinguish between vacuity of a property and of an assertion attempt. Property vacuity is defined in 16.14.8 Nonvacuous evaluations. What is indeed misleading is the first (and the following) sentence of this subclause:

"An evaluation attempt of a property is either vacuous or nonvacuous."

IMO, properties do not have attempts, but only assertions do. Therefore, it would be more appropriate to say: "A property evaluation is either vacuous or nonvacuous."

If we fix this, then the definition of positive and negative vacuity starts working. Consider the property not not 0 |-> 1. The inner property vacuously succeeds. The property not 0 |-> 1 vacuously fails, and the outer property again vacuously succeeds. Same situation is with reject_on. Had we not defined not 0 |-> 1 to fail vacuously, not not 0 |-> 1 would non-vacuously succeed.

As for assertion attempts, I don't think it makes sense to report their vacuous failure separately.

Thanks,
Dmitry

From: Ben Cohen [mailto:hdlcohen@gmail.com]
Sent: Monday, February 13, 2012 20:18
To: Korchemny, Dmitry; sv-ac@eda-stds.org
Cc: Eduard Cerny
Subject: [sv-ac] Notes of false vacuity + NO Meeting on Tuesday

Dmitry,
Actually, I got that issue of simulation statistics and vacuous fail resolved thanks to your help. We don't need a meeting. Just for the record, what is confusing in the LRM is the vacuity statements and the true/false statements on the not and the reject_on operators. As we often talked about,in our meeting, vacuity and true/false are separate notions. Thus, the LRM infers the notion of "false vacuity", or fail "vacuously" . For example:
  not( 0 |-> p) is both false and vacuous.
What confused me is my concept (or misconception?) that if a property is vacuous, it is because it is not meaningful in terms of statistics, that is is why it is vacuous. So when (not( 0 |-> p) ) contributes to the statistics, it just feels odd, just from the definition of vacuity. If I truly wanted a vacuous property to fail for the not and reject_on operators, I envisioned something like the following (assuming that anything vacuous is not counted) :
    not( a |-> p) and a // If a==0, we get vacuous for (a |->p) ANDed with a nonvacuous false.
    reject_on(a) p and !a[*] // if a==0, p gets evaluated. If a==1, we get a vacuous (reject_on(a) p) ANDed with a nonvacuous false.

So, in essence, even though my reasoning sounded right (I think!) this is not how it is (loosely I think) defined in the LRM. There is no point in pushing it. However, In the next iteration of 1800, it might be worth to clarify this notion of "false vacuity" because it does exist -- A property can be both: false (e.g., 16.12.2 Negation property) and vacuous (e.g., 16.14.8 d), and it is not explicitly clear when a false vacuously is counted in the statistics (can you point to the section for me?).

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.