RE: [sv-ac] RE: review 1682

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.