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

Hi Tej,
 
I think that it is correct in the proposal. [=] binds more strongly than ##. See Table 16-24 in Draft 3.
 
ed


________________________________

	From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Singh, Tej
	Sent: Monday, June 04, 2007 2:33 PM
	To: Korchemny, Dmitry; sv-ac@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 <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.