RE: [sv-ac] RE: review 1682

Hi Ed and SV-AC,

SV-EC just spent the last 6 months working through issues
with Clocking and Program blocks (See Mantis #890)

The main issue was that the P1800-2005 description of those
constructs wasn't thorough enough to guarantee consistent
behavior across  different tools.

This was caused by a couple factors:
 - Assumptions about methodology and design construction
 - Lack of attention to describing what happened when the
   assumptions didn't hold

If you guys end up going with something like the proposal
in 1682, I strongly encourage you to be rigorous in your
analysis of what happens when your input assumptions don't hold.

Also, if you can try to make the proposal more general in nature,
and less based on restrictions on user input, it will have
more value and be a better enhancement to the language.

Requiring simulators to check that values seen in the previous
time unit's Observed Region match the next time unit's Preponed
region will potentially be a huge overhead.  I urge you to find
another way.

In addition, there are many ways that a simulator can perform
multiple iterations of the big loop in Figure 9-1.  It can even
happen that an assertion's clock is kicked multiple times
during iterations of that big loop.  

All these issues should be considered if you ask that somehow
the simulator grab a sample during a non-postponed region of
the current time step, and somehow later validate that indeed
it was the final (postponed) value during that timestep.

To me, that's what postponed is all about.
It seems it would be simpler and safer to run the assertions in
the future timestep, when the $next value is reliably known.
I think you will avoid a lot of games and corner cases that way.

Regards,
Doug


> -----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.