RE: [sv-ac] RE: review 1682

Hi Manisha,

I think that the simulators can check that the value did not change
between observed region and the sampled value in the next time step. 

ed

> -----Original Message-----
> From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com] 
> Sent: Friday, February 23, 2007 4:53 PM
> To: Eduard Cerny; Doron Bustan
> Cc: Thomas.Thatcher@Sun.COM; sv-ac@eda-stds.org
> Subject: RE: [sv-ac] RE: review 1682
> 
> Hi,
> 
> I think the current definition of these functions is really confusing.
> Since signal values can change in the reactive region (after Observed
> region), Observed value may not be next sampled value. I guess the
> assumption is that users will use these functions only for the signals
> for which Observed region value is same as Sampled value in the next
> time step ?? The current proposal does not say that clearly. 
> Since there
> is no way for a simulator to check if this assumption is valid, the
> users may not get the results they expect.
>  
> Manisha
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org 
> [mailto:owner-sv-ac@server.eda.org] On
> Behalf Of Eduard Cerny
> Sent: Friday, February 23, 2007 12:49 PM
> To: Doron Bustan; Eduard Cerny
> Cc: Thomas.Thatcher@Sun.COM; sv-ac@server.eda-stds.org
> Subject: RE: [sv-ac] RE: review 1682
> 
> Hi Doron,
> but simulation must support it too. As I mentioned earlier, 
> if we define
> it as the sampled value in the next time step, the danger is that each
> simulator will implement different restrictions to make it more
> efficient. But if that's OK, then changing it to what you 
> want is easy,
> I just look up my older version of the document :-)
> 
> Best regards,
> ed
>  
> 
> > -----Original Message-----
> > From: Doron Bustan [mailto:dbustan@freescale.com]
> > Sent: Friday, February 23, 2007 3:07 PM
> > To: Eduard Cerny
> > Cc: Thomas.Thatcher@Sun.COM; sv-ac@eda-stds.org
> > Subject: Re: [sv-ac] RE: review 1682
> > 
> > Hi Ed, Tom,
> > 
> > I can understand the implementation difficulties. My view 
> is that the 
> > sampling semantics that guarantees a well defined, unique 
> evaluation 
> > of a given assertion on a given computation, is a valuable asset of 
> > SVA. I think that there should be a very good reason to 
> break it, and 
> > that the next time functions are important enough.
> > 
> > I prefer functions to which the  de-facto support is only in formal 
> > tools.
> > 
> > Doron
> > 
> > Eduard Cerny wrote:
> > 
> > >Hi Tom,
> > >
> > >the result should be equivalent to using the sampled value
> > from the next
> > >time step. That can be achieved by different means. One is
> > to delay the
> > >evaluation of the assertion till the next time step (which 
> I do not 
> > >like). Another one is as stated in the proposal, namely,
> > read the value
> > >in the observed region. That, however, imposes certain 
> constraints on
> 
> > >the way the design and the clock generation behaves, as 
> stated in the
> 
> > >proposal. I like thi better because it is easily 
> implementable and in
> 
> > >any case, mainly used in hybrid verif. methodologies where both 
> > >simulation and formal may be used.
> > >
> > >We will have to decide which way to go... as a group.
> > >
> > >Bestest,
> > >ed
> > >
> > >
> > >  
> > >
> > >>-----Original Message-----
> > >>From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of 
> > >>Thomas Thatcher
> > >>Sent: Friday, February 23, 2007 12:25 PM
> > >>To: sv-ac@eda-stds.org
> > >>Subject: Re: [sv-ac] RE: review 1682
> > >>
> > >>Hi Ed, Doron,
> > >>
> > >>But how would it be possible to use the sampled value 
> from the next 
> > >>time step in a simulation environment?  The simulator
> > hasn't got there
> > >>yet!
> > >>
> > >>As I understand it, a next value function like $isrising 
> will work 
> > >>by comparing the observed region value with the $sampled value.
> > >>Is my understanding correct?
> > >>
> > >>
> > >>Tom
> > >>
> > >>
> > >>
> > >>
> > >>
> > >>Eduard Cerny wrote On 02/22/07 12:52,:
> > >>    
> > >>
> > >>>Hi Doron,
> > >>>
> > >>>I understand exactly what you mean  and this is why the
> > >>>      
> > >>>
> > >>constraints on
> > >>    
> > >>
> > >>>the behavior for this to work were imposed. If everybody
> > >>>      
> > >>>
> > >>agrees that it
> > >>    
> > >>
> > >>>should be the sampled value from the next time step, 
> fine (I had an
> 
> > >>>earlier version of the document that stated that). Let's
> > >>>      
> > >>>
> > >>discuss it more
> > >>    
> > >>
> > >>>with others involved.
> > >>>
> > >>>ed
> > >>>
> > >>>
> > >>>      
> > >>>
> > >>>>-----Original Message-----
> > >>>>From: Doron Bustan [mailto:dbustan@freescale.com]
> > >>>>Sent: Thursday, February 22, 2007 3:02 PM
> > >>>>To: Eduard Cerny
> > >>>>Cc: sv-ac@eda-stds.org
> > >>>>Subject: Re: review 1682
> > >>>>
> > >>>>Hi Ed,
> > >>>>
> > >>>>but we do expext the conditions to change -
> > >>>>
> > >>>>"Under the conditions stated in the document, the value in the 
> > >>>>observedregion should be the same as the sampled value 
> in the next
> 
> > >>>>time step"
> > >>>>
> > >>>>what if there is an assignment in the re-NBA region?
> > >>>>
> > >>>>I prefer the performance penalty with the clean semantics.
> > >>>>
> > >>>>Doron
> > >>>>
> > >>>>Eduard Cerny wrote:
> > >>>>
> > >>>>
> > >>>>        
> > >>>>
> > >>>>>Hi Doron,
> > >>>>>
> > >>>>>1. This would have to be the sampled value from the next
> > time step.
> > >>>>>Under the conditions stated in the document, the value in
> > >>>>>          
> > >>>>>
> > >>>>the observed
> > >>>>
> > >>>>        
> > >>>>
> > >>>>>region should be the same as the sampled value in the next
> > >>>>>          
> > >>>>>
> > >>>>time step. We
> > >>>>
> > >>>>        
> > >>>>
> > >>>>>could state it as sampled value in the next time step,
> > >>>>>          
> > >>>>>
> > >>however, that
> > >>    
> > >>
> > >>>>>requires shifting the evaluation of the assertion to the
> > >>>>>          
> > >>>>>
> > >>>>next time step
> > >>>>
> > >>>>        
> > >>>>
> > >>>>>and possible performance penalty, or do what is stated now
> > >>>>>          
> > >>>>>
> > >>under the
> > >>    
> > >>
> > >>>>>hood and potentially have differences between simulators,
> > >>>>>          
> > >>>>>
> > >>>>both of which
> > >>>>
> > >>>>        
> > >>>>
> > >>>>>I wanted to avoid.
> > >>>>>
> > >>>>>2. Yes, that can be changed.
> > >>>>>
> > >>>>>3. This proposal does not really need global clocking, I
> > >>>>>          
> > >>>>>
> > >>>>could remove it
> > >>>>>from the example.
> > >>>>
> > >>>>        
> > >>>>
> > >>>>>Thanks,
> > >>>>>ed
> > >>>>>
> > >>>>>
> > >>>>>
> > >>>>>
> > >>>>>
> > >>>>>
> > >>>>>          
> > >>>>>
> > >>>>>>-----Original Message-----
> > >>>>>>From: Doron Bustan [mailto:dbustan@freescale.com]
> > >>>>>>Sent: Thursday, February 22, 2007 11:53 AM
> > >>>>>>To: Eduard.Cerny@synopsys.COM; sv-ac@eda-stds.org
> > >>>>>>Subject: review 1682
> > >>>>>>
> > >>>>>>Review of proposal 1682
> > >>>>>>==========================
> > >>>>>>
> > >>>>>>1. I don't have problem with restricting the use of these
> > >>>>>>            
> > >>>>>>
> > >>>>functions to
> > >>>>
> > >>>>        
> > >>>>
> > >>>>>> assertions, but then I think that $nextvalue should 
> return the 
> > >>>>>>sampled  value not the observed.
> > >>>>>>
> > >>>>>>2. Current definition of all other function return a 4
> > >>>>>>            
> > >>>>>>
> > >>>>state variable
> > >>>>
> > >>>>        
> > >>>>
> > >>>>>> e.g.  $isrising(expression) has the same effect as
> > >>>>>>       !lsb(expression)&& $nextvalue(lsb(expression)).
> > >>>>>>
> > >>>>>> so if "a" is X in the current cycle and 1 in the next
> > >>>>>>            
> > >>>>>>
> > >>cycle, then
> > >>    
> > >>
> > >>>>>> the result of $isrising(a) is Z. I recommend using the same 
> > >>>>>>language  as in the definition of $rose etc.
> > >>>>>>
> > >>>>>> The Table should represent 4 states variables.
> > >>>>>>
> > >>>>>>3. First example use global clocking which is not there yet...
> > >>>>>>
> > >>>>>>
> > >>>>>>  
> > >>>>>>
> > >>>>>>            
> > >>>>>>
> > >>>>>
> > >>>>>          
> > >>>>>
> > >>>>        
> > >>>>
> > >>--
> > >>------------------
> > >>Thomas J. Thatcher
> > >>Sun Microsystems
> > >>408-616-5589
> > >>------------------
> > >>
> > >>--
> > >>This message has been scanned for viruses and dangerous 
> content by 
> > >>MailScanner, and is believed to be clean.
> > >>
> > >>
> > >>    
> > >>
> > >
> > >  
> > >
> > 
> > 
> 
> --
> This message has been scanned for viruses and dangerous content by
> MailScanner, and is believed to be clean.
> 
> 
> 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.