RE: [sv-ac] 1731 description updated - "Sampled value functions with arbitrary clocks"

Hi Tej,

 

I agree with you. Attached the updated proposal. Please, ignore my previous mail.

 

Thanks,

Dmitry

 

________________________________

From: Singh, Tej [mailto:tej_singh@mentor.com] 
Sent: Monday, June 04, 2007 9:33 PM
To: Korchemny, Dmitry; sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] 1731 description updated - "Sampled value functions with arbitrary clocks"

 

Let n ¸ 1. If there exists 0 · i < j so that wi;j ; fg; fg j´ ((c&&e2) ##1 (c&&e2)[= n ¡ 1]), then $past
(e1; n; e2; c)[wj ] = e[wi]. Otherwise, $past(e1; n; e2; c)[wj ] is the result of evaluating the expression e1
using the initial values of the variables comprising the expression.
 

I think there is an issue in this definition when value of $past is being read at the same clock as the $past clock.

So for example consider the expression $past(e, 2, clk)) with clk edges occur at times t0, t1, t2, t3.....

 

Now consider the value of $past at time t2. The sequence (c&&e2) ##1 (c&&e2[=1]) matches on the path

between t1 and t2 inclusive. Which means the value of $past at t2 is the value of 'e' at t1 which is wrong.

It should be the value of 'e' at time t0.

 

I think the sequence expression should be 

 

(c&&e2) ##1 (c&&e2[=n-1])  ##1 TRUE

 

Regards

Tej

	 

	
________________________________


	From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Korchemny, Dmitry
	Sent: Monday, June 04, 2007 1:38 AM
	To: sv-ac@server.eda-stds.org
	Subject: [sv-ac] 1731 description updated - "Sampled value functions with arbitrary clocks"

	Hi all,

	 

	I updated 1731 proposal (attached here for convenience). The updated version also contains fixes in the formal semantics of extended booleans. Main points:

	* Functions $stable, $changed, $rose and $fell are now defined as derived from $past

	* The clock is now an argument in the sampled value function formal definition, instead of being part of the context

	* $past formal definition contains now enabling expression

	* cosmetic change in matched definition

	 

	It is not quite clear to me how the function $stable should be defined (the same question about $changed). I wrote the following definition:

	 

	$stable(e, c) <==> $past(e,1,1,c) === e

	 

	Wouldn’t it be better to define it as: $past(e,1,1,c) == e? The LRM is not clear about this.

	 

	Thanks,

	Dmitry

	
	-- 
	This message has been scanned for viruses and 
	dangerous content by MailScanner <http://www.mailscanner.info/> , and is 
	believed to be clean. 


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.