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.