RE: [sv-ac] #1381

Hi John/all,

I strongly agree with your comment regarding simulator etc ...
Implementation concerns should never be the driver for the semantics. 

As far as my suggested change on this thread for or/and to define
vacuous vs. nonvacuous, I have to qualify that it is a loop-hole comment
meaning in isolation it is valid -- the dual of the current version but
I did not really study exactly how it affects the induction and the
proposal as a whole so take it with a grain of salt. I say this because
I made peace with it once before, I forget now how :).

The attempt correction needs to be made, otw the whole condition
inference and pulling into assertion will be broken.

Thx.
-Bassam.

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Eduard Cerny
Sent: Friday, May 12, 2006 5:49 AM
To: john.havlicek@freescale.com; Eduard.Cerny@synopsys.COM
Cc: Manisha_Kulshrestha@mentor.com; dbustan@freescale.com; sv-ac@eda.org
Subject: RE: [sv-ac] #1381

Hello John,

welcome back to the discussions. I will reply in more detail (if still
needed) later.
Regarding immediate assserts - there is no notion of an attempt, it
executes in procedural code whenever the control reaches that point.

ed 

> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]
> Sent: Friday, May 12, 2006 3:59 AM
> To: Eduard.Cerny@synopsys.COM
> Cc: Manisha_Kulshrestha@mentor.com; dbustan@freescale.com; 
> sv-ac@eda.org
> Subject: Re: [sv-ac] #1381
> 
> Hi Ed and All:
> 
> I have been trying to follow the discussions, but not keeping up too 
> well.
> 
> I would like to see a coherent alternative inductive definition for 
> which the changes you are talking about for "or" and "not"
> are incorporated.
> 
> What is wrong with having a tool switch to control how much effort the

> simulator puts in looking for non-vacuity?  If we use the tool 
> performance as an excuse to break the definition, then I'm afraid we 
> will end up with a useless concept
> 
> Regarding the attempts, I'm not sure we have done the right thing so 
> far.
> 
> How does attempt counting work for immediate assertions?
> 
> 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, 11 May 2006 14:00:38 -0700
> > Thread-Topic: [sv-ac] #1381
> > Thread-Index: AcZ0+HWrfPq94WVFRB+ELcrxclutewAN3PHgAAMvt2A=
> > From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> > X-OriginalArrivalTime: 11 May 2006 21:00:40.0182 (UTC)
> FILETIME=[F5AC9160:01C6753D]
> > X-Virus-Status: Clean
> > X-MIME-Autoconverted: from quoted-printable to 8bit by
> server.eda.org id k4BL0cNj011904
> > Sender: owner-sv-ac@eda.org
> > 
> > Hello Doron et al,
> > 
> > A few comments regarding Manisha's comments:
> > 
> > 1. I think that the document defines only non-vacuous success by the

> > sentence on pp2 just above Section 177.13.4, even though it defines 
> > non-vacuous attempt too, without qualifying what kind of
> outcome of the
> > attempt takes place. I think this is useful. However, I agree with 
> > Manisha that the definition of the not operator is curious,
>  because to
> > succeed, property_expr must have non-vacuous attempt and not 
> > property_expr must succeed. But that can happen only when
> property_expr
> > fails.  Consequently, the failure must have been non-vacuous. How is

> > that defined?
> > 
> > 2. I'd agree, because the user must realize that there is a
> choice in
> > the property such that it can succeed if one of them has a vacuous 
> > success. Going beyond that can be unnecessarily costly.
> > 
> > 3. Not sure if it is clear what I meant - the condition is extracted

> > from the procedural block, a syntactic extraction, into a concurrent

> > property. hence vacuity etc. should apply the same way as
> if the user
> > wrote the property outside the always block and copied the condition

> > there manually.
> > 
> > I think that this also provides basis for extracting condition from,

> > say, combinational always blocks for assertions embedded
> there, provided
> > that the clock is explicitly specified in the assertion
> (which is what I
> > said earlier in agreement with Dmitry.)
> > 
> > Best regards,
> > ed
> > 
> > > -----Original Message-----
> > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf 
> > > Of Kulshrestha, Manisha
> > > Sent: Thursday, May 11, 2006 4:39 PM
> > > To: Doron Bustan; sv-ac@eda.org
> > > Subject: RE: [sv-ac] #1381
> > > 
> > > Hi Doron,
> > > 
> > > Few comments/questions on the proposal:
> > >  
> > > 1. So far LRM only had a concept of vacuous success but no vacuous

> > > failures. But in this proposal vacuous is not associated with 
> > > success or failures. Does that mean that we now have vacuous 
> > > success
> and vacuous
> > > failure ? If vacuous attempt is neither a success or failure, then

> > > should the action block be executed ? This question is
> more related to
> > > item (b) where you are defining not operator.
> > > 
> > > 2. Regarding (c) p1 or p2, I have a problem with this. 
> The simulator
> > > should not be forced to keep the evaluation attempt of a
> operand alive
> > > if the other operand has been determined to HOLD.
> > > Say an attempt started at t then suppose at t+1 simulator 
> > > determies that
> > > p1 holds vacously. Also assume that at t+10 simulator determies 
> > > that P2 holds non-vacuously. So, eventhough the simulator has 
> > > determined at time
> > > t+1 that the property 'p1 or p2' HOLDS at time t, its been
> > > asked to keep
> > > the evaluation of p2 alive to determine if 'p1 or p2' HOLDS 
> > > vacuosly or non-vacuously.
> > > 
> > > 3. Page3 section 17.3.5, I agree with Ed and Bassam that
> evaluation
> > > attempt should not be dependent on the enabling condition.
> > > 
> > > Thanks.
> > > Manisha
> > > 
> > > 
> > 
>