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

Hi Dmitry,

One more minor fix:

Heading  "18.2 Checker declaration"

Should be "16.18.2 checker declaration"

Tom

Korchemny, Dmitry wrote On 11/22/07 04:22 AM,:
> 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
------------------

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