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.