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

Hi Surya,

why do you see a contradiction? Page 408 deals with vacuity, while the annex shows logical equivalence. You also have under (d)
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

Non-vacuity is not affected by negation.

Best regards,
ed

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"

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.

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 |=> matches with item (j) and (k) for #-# and #=#. 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.

Again, am I missing something here?

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

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