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

Hi Bassam,

That is correct, but then you can also continue looking for vacuity in
the 2nd term, etc., until you reach something that is not an implication
anymore.

ed
 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Bassam Tabbara
> Sent: Thursday, February 23, 2006 12:47 PM
> To: sv-ac@eda.org
> Cc: dmitry.korchemny@intel.com
> Subject: RE: [sv-ac] Porposal assertion action control tasks
> 
> 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
> >  
> > 
> > > -----Original Message-----
> > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of 
> > > Kulshrestha, Manisha
> > > Sent: Wednesday, February 22, 2006 11:56 AM
> > > To: Korchemny, Dmitry; sv-ac@eda.org
> > > Subject: RE: [sv-ac] Porposal assertion action control tasks
> > > 
> > > Hi Dimitry,
> > > 
> > > The answer to question (2) is 'no'. 
> > > 
> > > As per LRM: "The disable iff clause allows preemptive 
> resets to be 
> > > specified. For an evaluation of the property_spec, there is an 
> > > evaluation of the underlying property_expr. If prior to the 
> > > completion of that evaluation the reset expression becomes true, 
> > > then the overall evaluation of the property_spec is true."
> > > 
> > > So, in this case 'rst' will be checked before 'a' and the 
> property 
> > > will have a disabled success. Since $assertdisableoff has been 
> > > called for this scope, the pass action 'action1' will not execute.
> > > 
> > > I also agree that we need more clear definition of 
> vacuous success.
> > > Specially in the cases of multiple implication operators and also 
> > > when implication is used along with other operators (and, 
> or etc.).
> > > 
> > > Thanks.
> > > Manisha
> > > 
> > > -----Original Message-----
> > > From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
> > > Sent: Wednesday, February 22, 2006 1:46 AM
> > > To: Kulshrestha, Manisha; sv-ac@eda.org
> > > Subject: RE: [sv-ac] Porposal assertion action control tasks
> > > 
> > > Hi Manisha,
> > > 
> > > Here are my comments:
> > > 
> > > 1) To define the action of $asservacuouson/of for 
> assertions we need
> 
> > > first a clear definition of vacuous success of an assertion.
> > > 
> > > 2) $assertdisabledon/off for assertions. Let's have the following
> > > property:
> > > 
> > > assert property (disable iff(rst) a) action1 else action2;
> > > 
> > > Suppose both rst and a are high and $assertdisableoff has been
> issued.
> > > Will action1 still take place?
> > > 
> > > 3) cover statement. As I wrote in my previous mail, the 
> definition 
> > > of cover statement itself needs a refinement. In my proposal the 
> > > notions of vacuous and disabled success for cover directives are 
> > > irrelevant.
> > > 
> > > 4) I definitely think that this is another errata item 
> (if you are 
> > > talking about #805)
> > > 
> > > Thanks,
> > > Dmitry
> > > 
> > > 
> > > -----Original Message-----
> > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of 
> > > Kulshrestha, Manisha
> > > Sent: Tuesday, February 21, 2006 7:25 PM
> > > To: sv-ac@eda.org
> > > Subject: RE: [sv-ac] Porposal assertion action control tasks
> > > 
> > > Hi All,
> > > 
> > > I am including a proposal for controlling action block execution. 
> > > Please send your feedback. Do we need another errata on 
> this issue 
> > > or this proposal can be added to the errata on disable iff (which 
> > > already has another proposal).
> > > 
> > > Thanks.
> > > Manisha
> > > 
> > > 
> > 
> 
>