RE: [sv-ac] Re: [SV-AC] IMPLIES / OR / AND / VACUITY TABLE

Hi Scott,

> Property success/failure (s/f) and vacuity/nonvacuity (v/nv) are separate concepts.

I am with you on this.

Regarding the table, I am not sure we can find a syntactic characterization that will give us that two equivalent formulas have the same vacuous results.

Take your preferred operators: implies2 and or1.
The formulas (p implies2 q) and ((not p) or q) are equivalent.
However, if p is true and vacuous and q is true and nonvacuous we get that
(p implies2 q) is vacuous (row 12 in table 1), whereas
((not p) or q) is non-vacuous (row 4 in table 2).

I think that if we are to make changes in the definition of vacuity we should first find a good semantic definition, then we can see if we can provide a syntactic characterization for it. As mentioned earlier, I think that temporal antecedent failure is a good candidate. This is since it is not affected by how the events are specified in the given formula, but rather how they are ordered in time. If an event fails to happens when expected at time t, clearly all events that are expected to hold at time t'>t do not affect the evaluation of the formula. And changing the way the formula is written will not change the order of the events (without changing the over whole set of traces satisfying the property).

Best,
Dana

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Little Scott-B11206
Sent: Wednesday, October 06, 2010 9:59 PM
To: ben@systemverilog.us; Korchemny, Dmitry; sv-ac@eda.org
Subject: RE: [sv-ac] Re: [SV-AC] IMPLIES / OR / AND / VACUITY TABLE

Blast! I am not smart enough to save my final edits before attaching it. Here is a version that doesn't break the tables across the pages.

Thanks,
Scott

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Little Scott-B11206
Sent: Wednesday, October 06, 2010 2:50 PM
To: ben@systemverilog.us; Korchemny, Dmitry; sv-ac@eda.org
Subject: RE: [sv-ac] Re: [SV-AC] IMPLIES / OR / AND / VACUITY TABLE

Hi Ben:

I have attached a prettied up version of the notes I mentioned yesterday. It should be noted that I have been thinking about this from a theoretical perspective. One thing that should likely be considered is which cases are of practical importance. I started thinking about that a bit, but I haven't come to any strong conclusions. I will continue thinking about it when I have some more time.

You sent an e-mail regarding the definition of vacuity earlier today. I should likely give my perspective which may give some clue as to the origin of the statements in the attached document. Property success/failure (s/f) and vacuity/nonvacuity (v/nv) are separate concepts. Each property will have a s/f and a v/nv result. The v/nv result gives additional information about the "quality" of the s/f result. The v/nv result should only be nv when all conditions required for the s/f result are determined by nv results.

Oh, I haven't carefully checked these notes for correctness. Please let me know if you find any errors.

Thanks,
Scott

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben cohen
Sent: Tuesday, October 05, 2010 12:18 PM
To: Korchemny, Dmitry; sv-ac@eda.org
Subject: [sv-ac] Re: [SV-AC] IMPLIES / OR / AND / VACUITY TABLE

On Tue, Oct 5, 2010 at 9:45 AM, ben cohen <hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>> wrote:

See attached table.
It needs work, but it is something that I would like to have clarified.
Ben

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