[sv-ac] RE: Issue 2578: Vacuity definition

I tend to agree with Dmitry.

ed

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Korchemny, Dmitry
Sent: Thursday, August 11, 2011 11:15 AM
To: Little Scott-B11206; sv-ac@eda-stds.org
Subject: [sv-ac] RE: Issue 2578: Vacuity definition

The LRM essentially says that the expression is non-vacuous if some of its subexpressions are non-vacuous. If you want to change this, we need to update all the definitions accordingly. Of course, there are different approaches to the vacuity definition.

Thanks,
Dmitry

From: Little Scott-B11206 [mailto:B11206@freescale.com]
Sent: Thursday, August 11, 2011 18:08
To: Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: RE: Issue 2578: Vacuity definition

Hi Dmitry:

That is correct. The LRM isn't consistent, and I don't think we can make it so.

Thanks,
Scott

From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
Sent: Thursday, August 11, 2011 10:04 AM
To: Little Scott-B11206; sv-ac@eda-stds.org
Subject: RE: Issue 2578: Vacuity definition

Hi Scott,

But your concept is not consistent with the LRM. E.g.,

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.

Regards,
Dmitry

From: Little Scott-B11206 [mailto:B11206@freescale.com]
Sent: Thursday, August 11, 2011 16:18
To: Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: RE: Issue 2578: Vacuity definition

Hi Dmitry:

Can you provide some justification for why you think the given definition doesn't work? To me this is one of those areas where sometimes you want the definition to be one way and sometimes you want it to be the other way. It sort of depends on how you look at vacuity...

I personally prefer the way it is currently written as I feel it is a higher bar for something to be declared nonvacuous. What you suggest allows the property in the antecedent to be vacuous while the overall property could be nonvacuous. That definition feels a bit weak to me. When I get a result of nonvacuous I want to know that all of the constituent parts also have nonvacuous evaluations.

Thanks,
Scott

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Korchemny, Dmitry
Sent: Thursday, August 11, 2011 7:42 AM
To: sv-ac@eda-stds.org
Subject: [sv-ac] Issue 2578: Vacuity definition

Hi all,

I am sorry to reopen the discussion about a resolved issue. Should have done it at the last meeting. There are two problems that I would like to discuss.

1. The following vacuity conditions for implies operator were suggested:

* If the antecedent is false, then (P1 implies P2) should be vacuous.

* Also, if the antecedent is vacuous, then (P1 implies P2) is vacuous.

* Also, if the antecedent is nonvacuous true, then (P1 implies P2) is nonvacuous if consequent is nonvacuous

My question is why the second condition has been added. If P1 is vacuously true, it does not mean that P1 implies P2 is vacuous.

2. Whatever the reply to my first question be, F.5.3.3 should be updated accordingly.

Thanks,
Dmitry
---------------------------------------------------------------------
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.
---------------------------------------------------------------------
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.