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

Hi Tej,
 
sorry, I missed the shift after the original sequence but saw the change in parentheses... ;-(
 
I think that you are right regarding the shift back by 1 clock tick.
 
Best regards,
ed


________________________________

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