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

*PLEASE READ EMBEDDED COMMENTS BELOW: *
:

On Mon, Feb 13, 2012 at 10:42 AM, Korchemny, Dmitry <
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".
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).

> 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.
 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?
Where in the LRM can we deduce that the *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.
:)
Ben

> 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* <http://www.mailscanner.info/>, and is
> believed to be clean.
>

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