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

From: Korchemny, Dmitry <dmitry.korchemny_at_.....>
Date: Mon Dec 03 2007 - 01:41:38 PST
Fixed.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Thomas Thatcher
Sent: Tuesday, November 27, 2007 8:17 PM
To: Korchemny, Dmitry
Cc: sv-ac@server.eda.org
Subject: 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.
---------------------------------------------------------------------
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.
Received on Mon Dec 3 01:42:26 2007

This archive was generated by hypermail 2.1.8 : Mon Dec 03 2007 - 01:42:43 PST