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.