RE: [sv-ac] Questions on "16.15.8 Nonvacuous evaluations"

<forwarding bounced email from John Havlicek>

-------- Original Message --------

Subject: RE: [sv-ac] Questions on "16.15.8 Nonvacuous evaluations"
Date: Mon, 5 Apr 2010 07:06:10 -0700
From: "Havlicek John-R8AAAU" <r8aaau@freescale.com>
To: "Eduard Cerny" <Eduard.Cerny@synopsys.com>,
         "Surya Pratik Saha" <spsaha@cal.interrasystems.com>,
         "sv-ac@server.eda.org" <sv-ac@eda.org>
Cc: "Vijeta Kashyap" <vijeta@interrasystems.com>,
         "Havlicek John-R8AAAU" <R8AAAU@freescale.com>

Hi Surya:

Ed has addressed your second question. Regarding the non-vacuity
definition for "and", the LRM is as the committee intended. We believe
it should not be necessary for both operands of "and" to have
non-vacuous evaluation, only one, in order to consider the "and"
evaluation to be non-vacuous. The two operands may not both be
satisfiable in a non-vacuous way. For example, prior to "if-else", one
might code in a style like

    (b |-> q1) and (!b |-> q2)

J.H.

________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Eduard Cerny
Sent: Monday, April 05, 2010 6:49 AM
To: Surya Pratik Saha; sv-ac@server.eda.org
Cc: 'Vijeta Kashyap'
Subject: RE: [sv-ac] Questions on "16.15.8 Nonvacuous evaluations"

Hi Surya,

=20

why do you see a contradiction? Page 408 deals with vacuity, while the
annex shows logical equivalence. You also have under (d)=20

An evaluation attempt of a property of the form not property_expr is
nonvacuous if, and only if, the

underlying evaluation attempt of property_expr is nonvacuous

=20

Non-vacuity is not affected by negation.

=20

Best regards,

ed

=20

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Surya Pratik Saha
Sent: Saturday, April 03, 2010 12:23 AM
To: sv-ac@server.eda.org
Cc: 'Vijeta Kashyap'
Subject: [sv-ac] Questions on "16.15.8 Nonvacuous evaluations"

=20

Hi,
IEEE 1800-2009 on page 408 says:
f) An evaluation attempt of a property of the form property_expr1 and
property_expr2 is nonvacuous if, and only if, either the underlying
evaluation attempt of property_expr1 is nonvacuous or the underlying
evaluation attempt of property_expr2 is nonvacuous.=20

It looks like a copy/paste of point above (e) for property_expr1 or
property_expr2.

Is this a type or am I missing something?

I have another question on same page. Description for item (h) for |->
and |=3D> matches with item (j) and (k) for #-# and #=3D#. Where as actual
difference between |-> and #-# is shown on page 1126, section F.3.4.3.6.
The definition on page 408 and derivation in section F.3.4.3.6 seem to
contradict.=20
=20
Again, am I missing something here?

Please let me know if there are already any Mantis items for this.

--=20
Regards
Surya

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