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.