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

Hi Ben,

Please, see my comments below.

Thanks,
Dmitry

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

Dmitry,
Embedded comments below. But before getting into them, I want to verify
what we would expect for statistical results on this model:
I need confirmation on my evaluation results.

module test_vacuity;
    bit clk, clk2, a, b, c, d, rst=0;
    initial forever #10 clk=!clk;
    initial forever #13 clk2=!clk2;
    default clocking cb_clk @ (posedge clk);
    endclocking
    property vac_true;
        1'b0 |-> 1'b1;
    endproperty : vac_true
    ap_vac_true: assert property(vac_true); // vacuous true, no pass or fail count updates
    ap_vac_false: assert property(not(vac_true)); // vacuous false, fail count updates
    ap_vac_not_false: assert property(not(not(vac_true))); // vacuous true, no pass or fail count updates
    ap_reject_on: assert property(reject_on(1'b1) 1'b1); // vacuous fail, fail count updates
endmodule : test_vacuity

[Korchemny, Dmitry] I agree with the comments in red.

PLEASE READ EMBEDDED COMMENTS BELOW:
:

On Mon, Feb 13, 2012 at 10:42 AM, Korchemny, Dmitry <dmitry.korchemny@intel.com<mailto:dmitry.korchemny@intel.com>> wrote:
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.
[Ben] 16.12.16 addresses 2 concepts thatare inline with what you are stating:
.. the case item property statements shall be evaluated and the evaluation of the case property statement from that start point succeeds and returns true (vacuously).
Thus, we have the concept of a property statement being evaluated and the concept of a return value of T/F.

16.14.8 addresses throughout the "An evaluation attempt of a property". We could change it in the future to
"an evaluation of a property".
[Korchemny, Dmitry] Agree.

If I get the jargon correctly, a property evaluates to either true of false, and in simulation the attempt evaluation of a property has the following fates: succeed nonvacuously (and pass counts are updated) , succeeds vacuously (no statistics collected) , fails nonvacuously (fail count updated), falls vacuously (fail count updated).
[Korchemny, Dmitry] I don’t completely agree. In simulation also property, and not “property attempt” is evaluated and succeeds or fails, both vacuously and non-vacuously. Assertions have attempts in simulation, and based on their results the corresponding counters are updated as you specified it.
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.
[Ben] So, in simulation, I would expect not (not (0 |-> 1)) should be vacuously true, and no statistics should be collected. However, If you break this evaluation in parts, there could be a different interpretation.
[Korchemny, Dmitry] According to my understanding, no statistics is collected in simulation for properties, but only for assertion attempts. For example, I would not expect in the following assertion:

assert property (a |-> nexttime b)

statistics to be collected separately for a, for next b, and for b, which are the properties composing this assertion.

 Specifically,
 (not (0 |-> 1 ) Fail that adds to statistics
 not(what has failed with statistics) == Pass that adds to statistics
I know that this sounds quirky, but would that be incorrect?
[Korchemny, Dmitry] In our example there is nothing that should be collected.
Where in the LRM can we deduce that the not( not(vacuous_property)) is vacuously true?
[Korchemny, Dmitry] vacuous_property is vacuous by definition. Here I assume it to be true, otherwise your example does not hold. According to 16.14.8 d) not(vacuous_property) is vacuously false. Applying 16.14.8 once more we get that not(not(vacuous_property)) is vacuously true.

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.
 [Ben] The LRM defines when something is vacuous or nonvacuous, but it does not define the term vacuity.
I agree with you about the reporting of vacuous failures. But in my mind, and from http://dictionary.reference.com/browse/vacuous
vac·u·ous
  has these definitions
1.
without contents; empty: the vacuous air.
2.
lacking in ideas or intelligence: a vacuous mind.
3.
expressing or characterized by a lack of ideas or intelligence;inane; stupid: a vacuous book.
4.
purposeless; idle: a vacuous way of life.
So a vacuous fail lacks purpose; why does it need to be counted in the statistics.
... But that is a vacuous issue since we cannot change the current interpretation in the LRM.
:)
[Korchemny, Dmitry] Without the concept of negative vacuity it would be impossible (applying syntactic, and not semantics, definitions of vacuity as it is done in the LRM) to define the positive vacuity of the property in the example above.

Ben
Thanks,
Dmitry

From: Ben Cohen [mailto:hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>]
Sent: Monday, February 13, 2012 20:18
To: Korchemny, Dmitry; sv-ac@eda-stds.org<mailto: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<http://www.mailscanner.info/>, and is
believed to be clean.

---------------------------------------------------------------------
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.