RE: [sv-ac] Mantis 1682: new proposal for Next-value functions

Hi Erik,

These are useful in both contexts, or so it seems, one where you do run
on design clock but wish to access the next value too. Implicitly in
formal verif. you would be running on the global clock in both cases
even if it is not explicitly visible. These functions are added mainly
for use by formal tools and so their intent is a bit lost outside that
context. I suspect that they will cause some difficulties in the other
committees ... 

There was also a proposal to name it not with _i, but with _g, for
global. Would that help?

Bestest
ed

> -----Original Message-----
> From: Seligman, Erik [mailto:erik.seligman@intel.com] 
> Sent: Wednesday, April 04, 2007 5:26 PM
> To: Eduard Cerny; sv-ac@eda-stds.org
> Cc: Korchemny, Dmitry
> Subject: RE: [sv-ac] Mantis 1682: new proposal for Next-value 
> functions
> 
> 
> OK, I think I see.  The _i signifies "immediate", to remind the user
> that this is an immediate global_clk, not whatever the clock of the
> property happens to be.  I'm still a little worried about an example
> like this though:
> 
> assert property (@clk $ischanging_i(sig) |-> $isrising_i(foobar))
>  		else $error("sig is not stable"); 
> 
> While the behavior is fully defined, it seems like there is some room
> for confusion by a user.  Was there any discussion of whether 
> we really
> need to support these in fully general assertions, or might it be
> possible to define them as valid only in cases where the local clock
> matches the global clock?  In other words, does the above example need
> to be supported, where 'clk' is not the global clock?
> 
> 
> -----Original Message-----
> From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com] 
> Sent: Wednesday, April 04, 2007 1:39 PM
> To: Seligman, Erik; Eduard Cerny; sv-ac@eda-stds.org
> Cc: Korchemny, Dmitry
> Subject: RE: [sv-ac] Mantis 1682: new proposal for Next-value 
> functions
> 
>  Hi Erik,
> 
> I deposited and attach a corrected file. The example you were 
> looking at
> was not updated for the "immediate future" function names. 
> 
> Your question may still be valid, however. We tried to avoid this
> problem by defining both past and future value functions that run only
> on the global clock. Therefore, hopefully, they would be sufficiently
> distinct from the regular sampled-value functions for the users to
> remember what they mean. 
> 
> Let me know if the explanation and also the intent is OK.
> 
> Best regards,
> ed
> 
> 
> > -----Original Message-----
> > From: Seligman, Erik [mailto:erik.seligman@intel.com]
> > Sent: Wednesday, April 04, 2007 3:35 PM
> > To: Eduard Cerny
> > Cc: Korchemny, Dmitry
> > Subject: RE: [sv-ac] Mantis 1682: new proposal for Next-value 
> > functions
> > 
> > 
> > Hi Ed--
> > I had a question about this proposal.
> > 
> > The example Assertion 1 you provide is:
> > 	assert property (@$global_clock $ischanging(sig) |->
> > $isrising(clk))
> > 		else $error("sig is not stable");
> > 	 
> > Suppose I had a slightly different property:
> > 	assert property (@clk $ischanging(sig) |-> $isrising(foobar))
> > 		else $error("sig is not stable");
> > 
> > As a design engineer, I might assume that $ischanging and $isrising 
> > are checking based on edges of 'clk', but if I understand the 
> > proposal, they will be based on $global_clk, even though 
> the property 
> > is checked on edges of clk.  Although the behavior is well-defined, 
> > I'm worried that this seems like it might lead to some confusion in 
> > real life.
> > 
> > Have you thought about this?  Or am I misunderstanding 
> something here?
> > 
> > 
> > 
> > -----Original Message-----
> > From: owner-sv-ac@server.eda.org
> > [mailto:owner-sv-ac@server.eda.org] On Behalf Of Eduard Cerny
> > Sent: Wednesday, April 04, 2007 10:21 AM
> > To: sv-ac@server.eda-stds.org
> > Subject: [sv-ac] Mantis 1682: new proposal for Next-value functions
> > 
> > Hello,
> > 
> > I have deposited a new proposal for next-value functions 
> that tries to
> 
> > address various concerns regarding the time when the value 
> is sampled 
> > and which clock is the default clock. It defines a new class of 
> > sampled-value functions, past and future, that run only on global 
> > clocking.
> > 
> > Best regards,
> > ed
> > 
> > --
> > 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.