Re: [sv-ac] Porposal assertion action control tasks

Hi Bassam:

Well, it seems that reasonable people can disagree on this.  :)

I think one can use only the top-level antecedent in defining vacuous
success and get a consistent definition.  

However, I don't think this gives us as useful a characterization
as looking at the concatenation of of the nested antecedents.  If
non-vacuous success is to be an indicator that the property has been
thoroughly exercised, then the evaluation needs to get through all the
nested antecedent conditions.

One might argue that the question of whether the property has been
thoroughly exercised is one of subproperty coverage and should not be
used to determine whether an action block executes.

I can see both points of view, but my gut feeling is that for 
nested implications we want the concatenation of nested antecedents
to be matched for non-vacuity.

Best regards,

John H.

> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0
> Content-class: urn:content-classes:message
> Date: Thu, 23 Feb 2006 09:47:29 -0800
> Thread-Topic: [sv-ac] Porposal assertion action control tasks
> Thread-Index: AcY3208ncjkPj1jxSLqwiOje+Ko7QQAxacig
> From: "Bassam Tabbara" <Bassam.Tabbara@synopsys.com>
> Cc: <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 23 Feb 2006 17:47:32.0364 (UTC) FILETIME=[38FD1CC0:01C638A1]
> X-Virus-Status: Clean
> X-MIME-Autoconverted: from quoted-printable to 8bit by server.eda.org id k1NHlY6T002918
> Sender: owner-sv-ac@eda.org
> 
> Hi Ed/John,
>  
> I am missing something. |-> is right associative, so for a |-> b |-> c
> chain it should be, assuming no bracketing done by user, a |-> (b |-> c)
> so really "a" would be the precondition in this case that affects
> vacuity. 
>  
> That said I don't see the ambiguity regardless of bracketing ... it's
> mostly covered by the description in LRM (cited by Shalom already may
> be) stating vacuity only applies to the top level implication i.e. that
> precondition's fail results in vacuous success of attempt.
>  
> Thx.
> -Bassam. 
> 
> 
> 
> --
> Dr. Bassam Tabbara
> Synopsys, Inc.
> (650) 584-1973
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
> Havlicek
> Sent: Wednesday, February 22, 2006 10:08 AM
> To: Eduard.Cerny@synopsys.COM
> Cc: Manisha_Kulshrestha@mentor.com; dmitry.korchemny@intel.com;
> sv-ac@eda.org
> Subject: Re: [sv-ac] Porposal assertion action control tasks
> 
> Hi Ed:
> 
> I would like first to understand the technical issues.  We can figure
> out later what to write in the LRM--in Section 17 or in Annex E.
> 
> I think that we should try to write an inductive definition that handles
> all cases and get it to match our intuition for the cases in which we
> have strong opinions.  I have a strong opinion that the inductive
> definition should match your example for nested implication operators.
> 
> We have been thinking about this some internally to Freescale.
> 
> Best regards,
> 
> John H.
> 
> > X-Authentication-Warning: server.eda.org: majordom set sender to 
> > owner-sv-ac@eda.org using -f
> > X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0
> > Content-class: urn:content-classes:message
> > Date: Wed, 22 Feb 2006 09:27:58 -0800
> > Thread-Topic: [sv-ac] Porposal assertion action control tasks
> > Thread-Index: 
> > AcYr7RovyWojkVyBTtuINlTYhpj0RwAGu7FgAsDQ4OAAILZRAAAQVEIQAAE2qyA=
> > From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> > X-OriginalArrivalTime: 22 Feb 2006 17:28:00.0059 (UTC) 
> > FILETIME=[53D3D0B0:01C637D5]
> > X-Virus-Status: Clean
> > X-MIME-Autoconverted: from quoted-printable to 8bit by server.eda.org 
> > id k1MHS86T002992
> > Sender: owner-sv-ac@eda.org
> > 
> > Hello,
> > 
> > I agree with Manisha on her interpretation of the effect of disable
> iff.
> > 
> > Regarding the vacuity in the presence of chains of implications, we 
> > could perhaps derive it by rewriting the chain into concatenations 
> > except for the last implication. I.e., (si is a sequence)
> > s1 |-> s2 |-> ... |-> sn |-> p
> > is equivalent to
> > s1 ##0 s2 ##0 ... ##0 sn |-> p   (similarly for |=>, with ##1
> > replacement)
> > 
> > In other words, if the concatenation s1 ##0 s2 ##0 ... ## sn does not 
> > match in the attempt, the success of the attempt is vacuous.
> > Defining vacuity once the attempt reaches successfully into p is 
> > another matter (assuming that all leading implications are taken out 
> > in front) and I do not think that we should attempt to put anything in
> 
> > the LRM for that case.
> > 
> > ed
> >  
> >