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

'primary inputs' of what?
What is their behavior?
 
Shalom


________________________________

	From: Korchemny, Dmitry 
	Sent: Thursday, February 07, 2008 10:03 AM
	To: Bresticker, Shalom; 'sv-ac@server.eda.org'
	Cc: 'sv-champions@server.eda.org'
	Subject: RE: [sv-ac] Mantis 1900 comments - Part 1
	
	

	Hi Shalom,

	 

	I rewrote this paragraph using the following language:

	 

	"The modeling mechanism in checkers is implemented using checker
variables and their assignments. Checker variables differ from regular
variables in that they may be both deterministic and nondeterministic.
The behavior of nondeterministic checker variables is similar to the
behavior of the primary inputs (see 16.18.6 for detailed information
about nondeterministic checker variable behavior in simulation and
formal verification). The nondeterministic checker variables are
referred to as free variables."

	 

	Thanks,

	Dmitry

	 

	
________________________________


	From: Bresticker, Shalom 
	Sent: Tuesday, January 29, 2008 2:11 PM
	To: Korchemny, Dmitry; 'sv-ac@server.eda.org'
	Cc: 'sv-champions@server.eda.org'
	Subject: 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  

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

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