RE: [sv-ac] vacuity

Hi,

I agree with Doron that we should not impose unnecessary load. If an EDA
tool maker wants to provide more information, be it, but it does not
have to be in the LRM.

Best regards,
ed
 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Doron Bustan
> Sent: Tuesday, April 11, 2006 9:07 AM
> To: Korchemny, Dmitry
> Cc: sv-ac@eda.org
> Subject: Re: [sv-ac] vacuity
> 
> Hi Dimitry,
> 
> I agree that the current definition may not give the user all the 
> information he wants.
> There are many different definitions of vacuity, most of them are far 
> more reach than
> the one we proposed.
> 
> Nevertheless, it is not clear that these definitions should be add to 
> the LRM.
> The downside of having more than one definition in the LRM is 
>  that it 
> overloads
> the reports requirements. You will expect a tool that is LRM 
> compliant 
> to able
> to report the successes according to each type of vacuity, it will 
> create a substantial
> overhead.
> 
> The advantage of the current proposal, is by its locality. 
> Meaning, the 
> non-vacuity
> is determined per attempt and ignores other attempts. This allows a 
> simple report, and
> a simple decision procedure for the execution of action blocks.
> 
> As for your proposal:
> 
> > * For $P = P_1 and P_2$ and assignment $L$, we have that $w,L\non P$
> > iff
> >      $w,L \non P_1$ and $w,L\non P_2$.
> > 
> >  * For $P = P_1 or P_2$ and assignment $L$, we have that $w,L\non P$
> > iff
> >      $w,L \non P_1$ and $w,L\non P_2$.
> 
> 
> I think it is too strict, because  some properties P1 and P2 cannot 
> succeed non vacuously
> at the same attempt.
> 
> For example for the derived operator
> 
> $if (b) P1 else P2 \equive (b |-> P1) and (!b |-> P2)$
> 
> there are no attempts in which both $(b |-> P1) $ and $(!b |-> P2)$
> hold non-vacuously.
> 
> regards
> 
> Doron
> 
> 
> 
> Korchemny, Dmitry wrote:
> 
> >Hi Doron,
> >
> >I agree with your proposal what the "top level" vacuity is 
> concerned. If
> >I understood it correctly, it essentially says that the vacuity is
> >defined according to the top level binary operator; I am ignoring the
> >reset issue for the sake of simplicity. To be more accurate, if the
> >antecedent of the property in the implication normal form 
> never matches,
> >and the property passes, it passes vacuously.
> >
> >Nevertheless the user is often interested to get the partial vacuity
> >data as well. Consider the following example:
> >
> >assert property ((a |-> b) and (c |-> d));
> >
> >Suppose that a happens in the input word, but c never 
> happens. According
> >to your definition the property passes non-vacuously, but the
> >information about the partial vacuity is also important. We need to
> >define some discrimination mechanism which will enable the exact
> >reporting. One option is to enumerate the implication 
> operators inside a
> >property in a lexicographical order.
> >
> >E.g., the reporting might be that the second implication executed
> >vacuously.
> >
> >Therefore I am suggesting defining to kinds of vacuity - 
> global vacuity
> >(= your definition) and partial vacuity (your definition with
> >appropriate modifications for or and and):
> >
> >* For $P = P_1 and P_2$ and assignment $L$, we have that $w,L\non P$
> >iff
> >     $w,L \non P_1$ and $w,L\non P_2$.
> >
> > * For $P = P_1 or P_2$ and assignment $L$, we have that $w,L\non P$
> >iff
> >     $w,L \non P_1$ and $w,L\non P_2$.
> >
> >What do you think?
> >
> >Dmitry
> >
> >-----Original Message-----
> >From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> >Doron Bustan
> >Sent: Tuesday, April 11, 2006 1:00 AM
> >To: sv-ac@eda.org
> >Subject: [sv-ac] vacuity
> >
> >I upload a new definition for vacuity.
> >The new definition differ from the old
> >one, at the "disable iff" operator.
> >
> >Doron
> >  
> >
> 
> 
>