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.