[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, and is
believed to be clean.