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

Hi Lisa,
 
please see my comments below.
 
Best...
ed


________________________________

	From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Lisa Piper
	Sent: Monday, June 04, 2007 10:59 AM
	To: Korchemny, Dmitry
	Cc: sv-ac@eda.org
	Subject: RE: [sv-ac] 1731 description updated - "Sampled value functions with arbitrary clocks"
	
	

	Hi Dmitry,

	 

	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.

	 

	But now that we are stating that the clock can be different than the clock used in the assertion, we also need to define the value of $rose in-between its clocks (e.g. I assume it holds its value between clock edges).   

	 

I think that this is defined by $past(e1; n; e2; c)[wj ] = e[wi]. There is not constraint on j.

	 

	 

	In  16.8.3, the following sentence needs to change to indicate that the initial values of the variables are used, not X:    "When these functions are called at or before the first clock tick of the clocking event, the results are computed by comparing the current sampled value of the expression to X."

	 

That has been done in Mantis 1550.

	 

	 

	When are these functions evalauated?  I assume they are evaluated in the reactive region using the sample values when they are in an assertion.  What about when they are used in HDL and/or an action block?  Do they reference the sampled values or the current values in HDL and action blocks?   It states that "A value change function detects the change in the sampled value of an expression."  so I assume that applies when these are used in an action block or HDL?  This means that an action block will reference the current values of variables with the exception of these system tasks, where the value is the same as that used in evaluating the assertion. 

	 

They are using $sampled values and thus return value when called based on these values. 
For RTL equivalence, there is another Mantis item: 1698, has some proposal in th ebugnote.

	 

	 

	Lisa

	 

	
________________________________


	From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Korchemny, Dmitry
	Sent: Monday, June 04, 2007 4:38 AM
	To: sv-ac@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.