FW: [sv-ac] my review

Hi Doron,

 

Forwarding you Shalom’s comment on your last question.

 

Dmitry

 

From: Bresticker, Shalom 
Sent: Thursday, September 25, 2008 10:55 PM
To: Korchemny, Dmitry
Subject: RE: [sv-ac] my review

 

I think it is better as currently appears in Draft 7.

 

Shalom

	 

________________________________

	From: Korchemny, Dmitry 
	Sent: Thursday, September 25, 2008 3:58 PM
	To: Bresticker, Shalom
	Subject: FW: [sv-ac] my review

	Hi Shalom,

	 

	Could you comment about the last question?

	 

	Thanks,

	Dmitry

	 

	From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Bustan, Doron
	Sent: Wednesday, September 24, 2008 11:35 AM
	To: sv-ac@server.eda.org
	Subject: [sv-ac] my review

	 

	16.17: Rules e and f are not consistent in the sense that rule e imply (not conclusively but in spirit) that any 

	sequence/property with unique semantic leading clock, can be used as a top level property in an

	assertion statement, while rule f, restricts it to instances. Example c4 is related.

	 

	 

	 

	Annex F.

	 

	F.3.2 at "| ( S ) // "parenthesized" form" the S is at a wrong font

	 

	 

	F.3.4.9 Checker variable assignment

	— rand t u = e = initial assume property (@1 u === e)

	— always @c u <= e = always assume property (@1 $future_gclk(u) === c ? e : u)

	 

	Should be

	 

	F.3.4.9 Checker variable assignment

	— rand t u = e =º initial assume property (@1 u === e)

	— always @c u <= e =º always assume property (@1 $future_gclk(u) === c ? e : u)

	 

	 

	 

	F.4.1:

	— Tp(sync_accept_on (b) p, c) º( (accept_on(b && c) Tp(p, c)).

	 

	Should be removed

	 

	 

	 

	F.4.2: I don't understand the fix (again 1938)

	 

	"For the definition of neutral satisfaction of assertion statements, b denotes the boolean expression representing the enabling condition for the assertion statement. Intuitively, b is derived from the conditions in the context causing a queued evaluation attempt of a procedural assertion statement (see 16.15.6), while b is 1 for a declarative assertion statement."

	 

	 

	 

	 

	F.4.3.1

	 

	At the definition of “w, b ╞ initial @(c) cover property T”,

	 

	 w0,i ╞ !c[*0:$]##1 c

	 

	Should be

	 

	w0,i ╞ |º !c[*0:$]##1 c

	 

	 

	 

	F.4.3.1

	 

	The ╞d relation is used before it is defined and with no wording explaining it. This is confusing.

	 

	 

	 

	F.4.3.1:

	 

	In the semantics for accept_on:

	 

	or for some 0 < j < |w|,

	 

	Should be

	 

	or for some 0 < ji < |w|,

	 

	 

	 

	 

	The answer to the question on page 1166, 1167 is yes (the reference is correct)

	 

	 

	 

	F.5.3: end of first paragraph

	 

	Shouldn't 

	 

	Only after this step is completed are the clock rewrite rules used.

	 

	Be

	 

	Only after this step is completed are the clock rewrite rules are used.

	 

	?

	 

	 

	 

	---------------------------------------------------------------------
	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. 

---------------------------------------------------------------------
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.