RE: [sv-ac] 1900 is reday for review

Hi Tom,

Thank you for your comments. I've fixed all the typos you pointed to
(checkers_071122dk.pdf). See my notes below regarding your comment #4.

Dmitry

-----Original Message-----
From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] 
Sent: Thursday, November 22, 2007 2:32 AM
To: Korchemny, Dmitry
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] 1900 is reday for review

Hi Dmitry,

I'm reading through the latest draft.  Here are my coments.

1.  Example, p 8-9
    The checker defined is "my_check", but the instance "check_outside"
is of
    a checker "check".  Should be "my_check"


2.   Example, p 10
	endchecker : check     should be:     endchecker :
check_in_context

3.  Second example, p 10
	endchecker : check     should be:     endchecker : check_illegal
	endchecker : check     should be:
			 endchecker : check_no_context_inference

4.  P. 13:  "In this example the free variable flag behaves as follows:"

    Change to:  "In formal verification, the free variable flag in this
		example behaves as follows"

[Korchemny, Dmitry] This is not exact. The specification requires that
the variable flag behaves as follows, this is not directly related to
formal verification. It is written "Formal analysis tools shall take all
possible legal behaviors of flag into account." and this statement is
true for FV of any model: it takes all possible legal behaviors if the
model into account.

I rewrote this statement as:
"In this example the following constraints are imposed on the free
variable flag:"

    Add:  "In simulation, the free variable flag may take on any value
at
	  any time, including combinations that could cause the assume
	  property statements in this example to fire"

[Korchemny, Dmitry] I don't think that in simulation flag values are
absolutely random (this might be a case for a "dumb" simulator, but a
smart simulator should try to satisfy the constraint or to consider all
the combinations). Therefore I added the following text:

"Simulation tools shall assign values to flag meeting the constraints
imposed by assumptions m1, m2, and m3. In case when a simulation tool is
unable to satisfy all assumptions, it shall fire a violation of
assumptions that could not be satisfied."

5.  Example, p 21
	endchecker : mycheck    should be:   endchecker my_check


Tom

Korchemny, Dmitry wrote On 11/21/07 04:08 AM,:
> Hi all,
> 
>  
> 
> I uploaded a new version of the checker proposal checkers_071120dk.pdf
>
<http://www.eda-stds.org/mantis/file_download.php?file_id=2813&type=bug>
> and I think it is ready for review. This proposal addresses comments
of
> several people. See the following threads for more information:
> 
> http://www.eda-stds.org/sv-ac/hm/5761.html
> 
> http://www.eda-stds.org/sv-ac/hm/5856.html
> 
> http://www.eda-stds.org/sv-ac/hm/5879.html
> 
>  
> 
> Thanks,
> 
> Dmitry
> 
> ---------------------------------------------------------------------
> 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* <http://www.mailscanner.info/>, and
is
> believed to be clean.

-- 
------------------
Thomas J. Thatcher
Sun Microsystems
------------------
---------------------------------------------------------------------
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.