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.