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

Miller,
Would this be a tool issue, meaning that the tool should report this
differentiation when I have property operators (e.g., or, and, implies)?
Ben
On Sun, Aug 14, 2011 at 1:02 PM, Miller Hillel-R53776
<r53776@freescale.com>wrote:

> From a coverage aspect there seems to be the need for an additional
> distinction. For 'or' the final goal will be to cover both properties and
> for 'and' we are interested in knowing which of the property expressions are
> already covered.
>
> *From*: ben cohen [mailto:hdlcohen@gmail.com]
> *Sent*: Sunday, August 14, 2011 02:32 PM
> *To*: Korchemny, Dmitry <dmitry.korchemny@intel.com>
> *Cc*: Little Scott-B11206; Eduard Cerny <Eduard.Cerny@synopsys.com>;
> sv-ac@eda-stds.org <sv-ac@eda-stds.org>
> *Subject*: Re: [sv-ac] RE: Issue 2578: Vacuity definition
>
> Dmitry,
> Therefore, to be consistent we need to state that p1 implies p2 is
> nonvacuous if p1 evaluates to true and p2 is nonvacuous. This leaves a
> question open whether we want *p1 to evaluate nonvacuously *(as in Ben’s
> proposal) * or not*. IMO if we don’t require non-vacuity of p1, we are
> more consistent with other definitions where at least one non-vacuity is
> required.
> [Ben] My understanding or interpretation of vacuity is as follows:
> *vacuity*: *A property is vacuous if it lacks serious purpose*. Vacuity
> rules are usually applied when implication operator is used. A property
> succeeds vacuously if the antecedent is FALSE. A property succeeds
> non-vacuously only if the consequent of the implication contributes to its
> success. Many applications have a triggering event that causes the thread to
> start (in the antecedent), and if the triggering event does not occur (i.e.,
> if false)* [this applies to the implication operator]*, then there is no
> need to further evaluate the thread (i.e., the rest of the property for that
> cycle), which is then considered vacuously TRUE.
>
> In P_implies: *assert property*(p1 *implies *p2); if p1 is vacuously
> true, the property of the assertion (i.e., the (p1 *implies *p2)lacks
> serious purpose. For example, if p1 is vacuous and p2 is trrue
> nonvacuously, reporting that the assertion P_implies was covered and
> succeeded is misleading. As a user of the reports, I would be forced to
> write other assertions to counter this false reporting of coverage, and that
> can get complicated.
>
> I agree that the definition of the *implies* vacuity should be as
> consistent with the definition of the suffix implication |-> vacuity. With
> the implication operator, the antecedent in non-vacuous because it is a
> sequence;
>
> Now, looking at the following 2 definitions in 16.15.8 Nonvacuous
> evaluations, I do question "f" for the "and" property operator.
> [16.15.8]* e) An evaluation attempt of a property of the form
> property_expr1 or 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.*
> [Ben] That makes sense because if p1 is vacuous (i.e, a don't case about
> it's outcome since it results contributes nothing to the assertion), then we
> would care about p2.
>
> [16.15.8] *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.*
> [Ben] That does not make sense because if p1 is vacuous (i.e, a don't
> case about it's outcome since it results contributes nothing to the
> assertion), then why would the true (NV) success p2.be the only criteria
> for a successful coverage? Example, let p1 define a successful datafetch and p2 define a bus transfer
> (e.g., p1: fetch_sequence |-> ##[1:4]rdy ##1 mem_data_valid)
> (e.g., p2: rdy ##1 bus_grant |-> ##[1:4]data_bus==mem[addr])
> In (*p1 and p2)*, it seems that for a good coverage, both of them need
> to be non-vacuously true. Thus, in the above example, if *fetch_sequence*fails, but we go ahead and evaluate p2, and it is non-vacuously true, then
> this
> *(p1 and p2)*counts toward the coverage. I maybe wrong, but that does not
> sound like an "and" operation to me.
> The point of all this: coverage.
> Ben Cohen
>
> On Sun, Aug 14, 2011 at 9:45 AM, Korchemny, Dmitry <
> dmitry.korchemny@intel.com> wrote:
>
>> Hi all,****
>>
>> ** **
>>
>> As Ben mentioned in one of his previous mails I think that the definition
>> of the *implies* vacuity should be as consistent with the definition of
>> the suffix implication |-> vacuity. The latter is given by the following
>> statement:****
>>
>> ** **
>>
>> h) An evaluation attempt of a property of the form *sequence_expression *
>> *|-> **property_expr *is****
>>
>> nonvacuous if, and only if, there is a successful match of the antecedent
>> *sequence_expression *and****
>>
>> the evaluation attempt of * property_expr *that starts at the end point
>> of the match is nonvacuous.****
>>
>> ** **
>>
>> Therefore, to be consistent we need to state that p1 implies p2 is
>> nonvacuous if p1 evaluates to true and p2 is nonvacuous. This leaves a
>> question open whether we want p1 to evaluate nonvacuously (as in Ben’s
>> proposal) or not. IMO if we don’t require non-vacuity of p1, we are more
>> consistent with other definitions where at least one non-vacuity is
>> required.****
>>
>> ** **
>>
>> Whatever the decision be, we need to update Annex F accordingly. Also,
>> this Mantis is a good opportunity to fix the first paragraph of 16.15.8: we
>> need to delete the sentence that I put into square brackets.****
>>
>> ** **
>>
>> An evaluation attempt of a property is either vacuous or nonvacuous. [In
>> the following, nonvacuous evaluation is described for the following kinds of
>> properties: sequence, negation, disjunction, conjunction, if–else,
>> implication, and instantiation.]****
>>
>> ** **
>>
>> Thanks,****
>>
>> Dmitry****
>>
>> ** **
>>
>> *From:* ben cohen [mailto:hdlcohen@gmail.com]
>> *Sent:* Friday, August 12, 2011 00:16
>>
>> *To:* Little Scott-B11206
>> *Cc:* Eduard Cerny; Korchemny, Dmitry; sv-ac@eda-stds.org
>> *Subject:* Re: [sv-ac] RE: Issue 2578: Vacuity definition****
>>
>> ** **
>>
>> Scott, ****
>>
>> Lots of good work with that table! Here's a 1st cut at my reactions. ****
>>
>> the underlying evaluation attempt of property_expr1 is true ****
>>
>> and the underlying evaluation attempt of property_expr1 or property_expr2
>> ****
>>
>> is nonvacuous.****
>>
>> 1 = ((not p) or q)****
>>
>> 2 = p |-> q (in this case column p we interpret 1 as a matching sequence
>> ****
>>
>> and 0 as not a matching sequence the vacuity information is ignored)*
>> ***
>>
>> 3 = definition in current proposal****
>>
>> 4 = definition in this e-mail****
>>
>> Prop=(a|->b implies c|->d);****
>>
>> p q 1 2 3 4 Evaluation****
>>
>> 0,V 0,V V V V V tv --****
>>
>> 0,V 0,N N V V V tv OK****
>>
>> 0,N 0,V N V V V tv OK****
>>
>> 0,N 0,N N V V V tv OK****
>>
>> 0,V 1,V V V V V tv OK ****
>>
>> 0,V 1,N N V V V tv OK ****
>>
>> 0,N 1,V N V V V tv OK ****
>>
>> 0,N 1,N N V V V tv OK ****
>>
>> 1,V 0,V V V V V fv OK ****
>>
>> 1,V 0,N N N V N f <<- CASE A: with 4, if antecedent is 1V, and ****
>>
>> consequent is 0N property is nonvacuous fail.*
>> ***
>>
>> With 3, property is vacuous fail ****
>>
>> 1,N 1,V N V V N t <<- CASE B: with 4, if antecedent is 1V, and ****
>>
>> consequent is 0N property is nonvacuous true.*
>> ***
>>
>> With 3, property is vacuous true ****
>>
>> 1,N 0,V N V V N f <<- CASE C: with 4, if antecedent is 1N, and ****
>>
>> consequent is 0V property is nonvacuous fail.*
>> ***
>>
>> With 3, property is vacuous fail ****
>>
>> 1,V 1,N N N V N t <<- CASE D: with 4, if antecedent is 1N, and ****
>>
>> consequent is 1N property is nonvacuous true.*
>> ***
>>
>> With 3, property is vacuous true****
>>
>> 1,N 0,N N N N N f OK****
>>
>> 1,V 1,V V V V V t OK ****
>>
>> 1,N 1,N N N N N t OK ****
>>
>> ** **
>>
>> Consider the property below****
>>
>> (get_cache_status && cache_entry[addr]==INVALID |-> ****
>>
>> request_main_mem_bus |-> main_mem_bus_ready) implies****
>>
>> (main_mem_bus_ready |-> ##[1:5] cache_entry[addr]==VALID);****
>>
>> *CASE A: if get_cache_status==0, and main_mem_bus_ready==1, *****
>>
>> * but cache_entry[addr]==0 then with 3 we fail 0N, *****
>>
>> * with 4 we're vacuous fail, or 0V *****
>>
>> *What do want? If I don't care about getting from the cache, why should *
>> ****
>>
>> *I fail nonvacuously? *****
>>
>> ** **
>>
>> ** **
>>
>> 16.13.7 Implies and iff properties****
>>
>> A property is an implies if it has the following form:****
>>
>> property_expr1 implies property_expr2****
>>
>> A property of this form evaluates to true if, and only if, ****
>>
>> either property_expr1 evaluates to false or****
>>
>> property_expr2 evaluates to true.****
>>
>> ** **
>>
>> ** **
>>
>> ** **
>>
>> ** **
>>
>> On Thu, Aug 11, 2011 at 1:04 PM, Little Scott-B11206 <
>> B11206@freescale.com> wrote:****
>>
>> Hi Ben:****
>>
>> ****
>>
>> The rewrite that I think is most appropriate is below:****
>>
>> ****
>>
>> the underlying evaluation attempt of property_expr1 is true and the
>> underlying evaluation attempt of property_expr1 or property_expr2 is
>> nonvacuous.****
>>
>> ****
>>
>> Unfortunately it isn’t like ((not p1) or p2) or like |->. ((not p1) or
>> p2) does not use the truth result of p1 to determine vacuity. This
>> definition above requires that p1 evaluate to true for the overall property
>> to be nonvacuous. The definition of |-> doesn’t have a vacuity result for
>> the antecedent so it can’t be used and that introduces differences with the
>> definition above.****
>>
>> ****
>>
>> Why don’t we make a table to make this more concrete. Hopefully the table
>> makes sense.****
>>
>> 0 = evaluates to false****
>>
>> 1 = evaluates to true****
>>
>> V = vacuous****
>>
>> N = nonvacuous****
>>
>> ****
>>
>> 1 = ((not p) or q)****
>>
>> 2 = p |-> q (in this case column p we interpret 1 as a matching sequence
>> and 0 as not a matching sequence the vacuity information is ignored)****
>>
>> 3 = definition in current proposal****
>>
>> 4 = definition in this e-mail****
>>
>> ****
>>
>> p q 1 2 3 4****
>>
>> 0,V 0,V V V V V****
>>
>> 0,V 0,N N V V V****
>>
>> 0,N 0,V N V V V****
>>
>> 0,N 0,N N V V V****
>>
>> 0,V 1,V V V V V****
>>
>> 0,V 1,N N V V V****
>>
>> 0,N 1,V N V V V****
>>
>> 0,N 1,N N V V V****
>>
>> 1,V 0,V V V V V****
>>
>> 1,V 0,N N N V N****
>>
>> 1,N 0,V N V V N****
>>
>> 1,N 0,N N N N N****
>>
>> 1,V 1,V V V V V****
>>
>> 1,V 1,N N N V N****
>>
>> 1,N 1,V N V V N****
>>
>> 1,N 1,N N N N N****
>>
>> ****
>>
>> What do you think? Do any of those definitions seem like what we should
>> have?****
>>
>> ****
>>
>> Thanks,****
>>
>> Scott****
>>
>> ****
>>
>> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben
>> cohen
>> *Sent:* Thursday, August 11, 2011 2:26 PM****
>>
>>
>> *To:* Little Scott-B11206
>> *Cc:* Eduard Cerny; Korchemny, Dmitry; sv-ac@eda-stds.org
>> *Subject:* Re: [sv-ac] RE: Issue 2578: Vacuity definition****
>>
>> ****
>>
>> So what rewrites you would like to see? ****
>>
>> Also, will (p1 implies p2) be same as ((not p1) or p2), or more like ****
>>
>> the implication operator where a false in the antecedent causes the (p1
>> implies p2) to be vacuous. ****
>>
>> The latter is what I want to see. ****
>>
>> I am open to suggestions on the rewrites. ****
>>
>> BTW, I won't be able to make the Tuesday meeting. ****
>>
>> Ben ****
>>
>> ****
>>
>> On Thu, Aug 11, 2011 at 10:13 AM, Little Scott-B11206 <
>> B11206@freescale.com> wrote:****
>>
>> Hi Ben:****
>>
>> ****
>>
>> See my response below.****
>>
>> ****
>>
>> Thanks,****
>>
>> Scott****
>>
>> ****
>>
>> *From:* ben cohen [mailto:hdlcohen@gmail.com]
>> *Sent:* Thursday, August 11, 2011 11:10 AM
>> *To:* Little Scott-B11206
>> *Cc:* Eduard Cerny; Korchemny, Dmitry; sv-ac@eda-stds.org
>> *Subject:* Re: [sv-ac] RE: Issue 2578: Vacuity definition****
>>
>> ****
>>
>> There is another more important issue: What do we really want from the
>> implies operator? ****
>>
>> ****
>>
>> [SL]: I would like something a bit more sane than is in the current LRM
>> although I also believe that the definitions in the LRM aren’t usable in
>> practice. I would be in favor of a major overhaul of all definitions if we
>> knew what that overhaul should look like. My impression based on previous
>> discussions is that we don’t.****
>>
>> ****
>>
>> The '09 definition is ****
>>
>> (p1 implies p2) is ((not p1) or p2)****
>>
>> With the update that we approved, I believe that the meaning is more like
>> ****
>>
>> p1 |-> p2 // with the |-> working on properties, and p1 starts at the
>> same time as p2, ****
>>
>> In other words, ****
>>
>> (p1 implies p2) is more like (p1 and p2), but ****
>>
>> if p1 fails, then (p1 implies p2) is vacuous ****
>>
>> That's a major redefinition. ****
>>
>> ****
>>
>> Here's what's in the new update, and a table used as an example. ****
>>
>> z) An evaluation attempt of a property of the form property_expr1 implies
>> property_expr2 is nonvacuous if, and only if, ****
>>
>> the underlying evaluation attempt of property_expr1 is true, ****
>>
>> the underlying evaluation attempt of property_expr1 is nonvacuous, ****
>>
>> and the underlying evaluation attempt of property_expr2 is nonvacuous ***
>> *
>>
>>
>> ****
>>
>> ****
>>
>> (a |-> b) implies (c -> d);****
>>
>> a b c d ****
>>
>> 0 x 0 x p1==vacuous, p2==vacuous (p1 implies p2) is vacuous**
>> **
>>
>> 0 x 1 0 p1==vacuous, p2==FALSE (p1 implies p2) is vacuous**
>> **
>>
>> [SL] There isn’t enough information in the above line to determine the
>> result. The antecedent c has a successful match, so the question is does
>> the evaluation of d have a vacuous or nonvacuous result? See my comment
>> about a vacuous fail below. The information needed in the table is truth
>> value and vacuity result for p1 and vacuity result for p2. The truth value
>> of p2 is irrelevant when computing vacuity based on the above definition
>> (although if c doesn’t match you know the vacuity result).****
>>
>> 0 x 1 1 p1==vacuous, p2==TRUE (p1 implies p2) is vacuous**
>> **
>>
>> 1 0 0 x p1==FALSE, p2==vacuous (p1 implies p2) is vacuous**
>> **
>>
>> 1 0 1 0 p1==FALSE, p2==FALSE (p1 implies p2) is vacuous**
>> **
>>
>> 1 0 1 1 p1==FALSE, p2==TRUE (p1 implies p2) is
>> vacuous ****
>>
>> -------------------NONVACUOUS CONDITIONS
>> -------------------------------
>> ****
>>
>> 1 1 1 0 p1==TRUE, p2==FALSE (p1 implies p2) is FALSE ***
>> *
>>
>> 1 1 1 1 p1==TRUE, p2==TRUE (p1 implies p2) is TRUE ****
>>
>> ****
>>
>> With Ed's comments: ****
>>
>> the underlying evaluation attempt of property_expr1 is true and the
>> underlying evaluation attempt of property_expr1 or property_expr2 is
>> nonvacuous. ****
>>
>> [Ben] but 1st part of sentence says "property_expr1 is true", ****
>>
>> 2nd part says "property_expr1 or property_expr2 is nonvacuous"****
>>
>> The ""property_expr1" is not needed because it must be true from 1st part.
>> True? ****
>>
>> ****
>>
>> [SL] Not true. It is possible for a property to evaluate to true and be
>> vacuous or false and vacuous. Vacuity and the result of the evaluation are
>> two different things. For instance, let’s say I have a property not(p |->
>> q) then if p doesn’t match I have a property that evaluates to false and is
>> vacuous. If I remove the not() then I have a property that evaluates to
>> true and is vacuous.****
>>
>> ****
>>
>> I think we have the same thing about this redefinition. ****
>>
>> p1 p2 (p1 implies p2) ****
>>
>> 0 0 vacuous****
>>
>> 0 1 vacuous****
>>
>> 1 0 fail ****
>>
>> 1 1 pass ****
>>
>> 1 V vacuous. ****
>>
>> ****
>>
>> I like this definition of the implies operator as it is more in line with
>> the |-> operator. ****
>>
>> But that is a big change, non-backward compatible.****
>>
>> ****
>>
>> [SL] I agree and prefer the definition in the current version of the
>> proposal. However, Dmitry points out that it isn’t consistent with the rest
>> of the LRM (e.g., the definitions for ‘and’ and ‘until’). We should
>> probably be consistent with what is there as I don’t think it is prudent to
>> change those definitions as well.****
>>
>> ****
>>
>> Ben ****
>>
>> ****
>>
>> ****
>>
>>
>> ****
>>
>> ****
>>
>> On Thu, Aug 11, 2011 at 8:22 AM, Little Scott-B11206 <
>> B11206@freescale.com> wrote:****
>>
>> Hi Ed, Dmitry:****
>>
>> ****
>>
>> Okay, that is fine. How about the following then…****
>>
>> ****
>>
>> the underlying evaluation attempt of property_expr1 is true and the
>> underlying evaluation attempt of property_expr1 or property_expr2 is
>> nonvacuous.****
>>
>> ****
>>
>> Thanks,****
>>
>> Scott****
>>
>> ****
>>
>> *From:* Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
>> *Sent:* Thursday, August 11, 2011 10:19 AM
>> *To:* Korchemny, Dmitry; Little Scott-B11206; sv-ac@eda-stds.org****
>>
>>
>> *Subject:* 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* <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. ****
>>
>> ** **
>> ---------------------------------------------------------------------
>> 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.