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

Hi Ed,
 
I am not talking about operator precedence. I understand that [=] binds more strongly than ##.
 
I am trying to point out that the [=n-1] repeat matches at the time when 'c&&e2' happens n-1th time.
In my example of $past(e, 2, clk), the sequence (c&&e2) ##1 (c&&e2[=1] holds tightly between t1 and t2.
which gives the wrong value of $past.
 
Do you agree?
 
Tej

________________________________

	From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com] 
	Sent: Monday, June 04, 2007 11:39 AM
	To: Singh, Tej; Korchemny, Dmitry; sv-ac@eda-stds.org
	Subject: 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.