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

Hi Ben:

Thanks for the comments.

When John Havlicek read the document he found a few errors (the primary
one being that I used q instead of p for the results of implies0). I
have attached a version that includes those updates. I didn't update
the notation though.

Thanks,

Scott

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Thursday, October 07, 2010 11:03 AM
To: Dana Fisman
Cc: Little Scott-B11206; Korchemny, Dmitry; sv-ac@eda.org
Subject: Re: [sv-ac] Re: [SV-AC] IMPLIES / OR / AND / VACUITY TABLE

Scott,

Good table, thanks.

I had trouble with your notation, so I modified it a bit, as shown in
the attached file. Basically, I replaced

!t with F

t with T

!nv with VA
I also added some minor comments.

Thanks,

Ben

On Wed, Oct 6, 2010 at 1:42 PM, Dana Fisman <Dana.Fisman@synopsys.com>
wrote:

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