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

if this is so problematic to understand vacuity maybe it is good idea to put
such true tables for all operators into LRM
 
DANiel

  _____

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Little
Scott-B11206
Sent: Friday, October 08, 2010 6:32 PM
To: ben@systemverilog.us; Dana Fisman
Cc: Korchemny, Dmitry; sv-ac@eda.org
Subject: 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  <http://www.mailscanner.info/> MailScanner, and is 
believed to be clean. 
-- 
This message has been scanned for viruses and 
dangerous content by  <http://www.mailscanner.info/> MailScanner, and is 
believed to be clean. 
-- 
This message has been scanned for viruses and 
dangerous content by  <http://www.mailscanner.info/> MailScanner, and is 
believed to be clean. 
 
-- 
This message has been scanned for viruses and 
dangerous content by  <http://www.mailscanner.info/> 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.