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