[sv-champions] RE: [sv-ac] Mantis 1900 comments - Part 1

I thought of that, but there is already a such a reference at the
beginning of the paragraph. Two such references so close together looks
awkward. On the other hand, it is not clear that the first reference is
relevant to understanding what 'undefined' means here.
 
Shalom


________________________________

	From: Korchemny, Dmitry 
	Sent: Tuesday, January 29, 2008 2:10 PM
	To: Bresticker, Shalom; 'sv-ac@server.eda.org'
	Cc: 'sv-champions@server.eda.org'
	Subject: RE: [sv-ac] Mantis 1900 comments - Part 1
	
	

	Will it be enough to add a reference to 16.8.6?

	 

	Thanks,

	Dmitry

	 

	
________________________________


	From: Bresticker, Shalom 
	Sent: Tuesday, January 29, 2008 2:07 PM
	To: Korchemny, Dmitry; 'sv-ac@server.eda.org'
	Cc: 'sv-champions@server.eda.org'
	Subject: RE: [sv-ac] Mantis 1900 comments - Part 1

	 

	Hi,

		 

		- 16.18.1 says, "Checker variables differ from regular
variables in that they may be both deterministic and nondeterministic.
They may have undefined or partially constrained values, while regular
variables are always deterministic in the sense that they contain only
one specific value at a time." I have not yet finished the proposal, but
what does 'undefined' mean here? It seems a little strange.

		[Korchemny, Dmitry] "Undefined" means that the variable
may contain any value of its type, and in formal verification when this
variable is used in an assertion, this assertion is checked for all
possible values of this variable. This is explained in 16.8.6:

		"A free variable may assume any value at every point in
time, similarly to an input of the design. Formal analysis tools shall
take into account all possible values of the free variables imposed by
the assumptions and assignments (see 16.18.6.1). Simulators shall assign
arbitrary values to the free variables consistent with the assumptions
and the assignments."

		[SB] Thanks, I think this should be clearer. 

		Shalom  


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