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

Hi,

I agree with John's point:

>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.

This is exactly our dilemma as one of our verification coverage goals is
to 
measure what events are covered/exercised and what are not
covered/exercised.

--Joseph


Joseph Lu
IC Verification Mgr
Altera Corp.
101 Innovation Dr.
San Jose, CA95134
Tel:408-5448694
Eamil:jlu@altera.com


-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
Havlicek
Sent: Thursday, February 23, 2006 10:36 AM
To: Bassam.Tabbara@synopsys.com
Cc: sv-ac@eda.org; dmitry.korchemny@intel.com
Subject: 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
> >  
> >