[sv-ac] JH D6 review items

Hi Folks:

My review items are in the attached file.

J.H.

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


1734
----

. F.3.2, p. 1116.  Change

     always @(b) assert property P ( T )

  to

     always @(b) assert property ( T )

. F.4.3.1, p. 1121.  Under "Disabling of top-level properties is defined as follows",
  in the case "For T = disable iff (b) P" there is an awkward line break in which 
  "w^{0,i-1}\bot^\omega |/= P"  is divided up with "w" at the end of one line and 
  "^{0,i-1}\bot^\omega |/= P" is at the beginning of the next line.  The "w" should
  be moved to the next line to keep this mathematical statement together.



1667 part 1
-----------

. 16.8.2, p. 321.  Cross reference mistakes.
  - First paragraph reference to 16.5.1 should be to 16.6.1.
  - Third paragraph references to 16.7 should be to 16.8 (2 places).
  - Third paragraph reference to 16.9 should be to 16.10.

. 16.8.2, p. 322.  I think 

     It shall be an error if there exists a match of the named
     sequence for which an inout or output local variable formal
     argument is unassigned at the completion of a match.

  should be changed back to 

     It shall be an error if there exists a match of the named
     sequence for which an inout or output local variable formal
     argument is unassigned at the completion of the match.

  Rationale:  When we say "there exists a match" we have identified
  that match.  Alternatively, one could change

     at the completion of a match

  to

     at the completion of that match

. 16.8.2, p. 323, example seq2_inlined.  There is a missing ")" that
  should appear after "v1 = lv".  In fact, "v1 = lv" should be 
  moved up as part of the preceding line, i.e. change

     ##1 (!b[*0:$] ##1 b && (data_out == lv),
     v1 = lv

  to

     ##1 (!b[*0:$] ##1 b && (data_out == lv), v1 = lv)

  This was a mistake in the 1667 proposal.

. 16.8.2, p. 323.  Change

     and later referenced the value

  to

     and later reference the value

  Rationale:  Grammar.  

  This was a mistake in the 1667 proposal.

. 16.10, p. 345.  In the second paragraph, first sentence, change

    is achieved by either by

  to

    is achieved by either

. 16.10, p. 345.  Second paragraph after Syntax 16-13, second sentence, change

     Initializationassignments

  to

     Initialization assignments

. 16.13, p. 353 and Annex A.2.10, p. 1067.  Change

     property_lvar_port_direction ::= input | inout | output

  to

     property_lvar_port_direction ::= input

  Rationale:  Directions inout and output are not allowed for property
  local variable arguments.  In general, a property does not have an
  endpoint at which it "matches" like a sequence, and there is no 
  control flow out of the property evaluation.

1667 part 2
-----------

None of the changes from 1667 part 2 has been implemented in Draft 6.


1668 part 1
-----------

. 16.10, Syntax 16-14.  Change

     | subroutine_call

  to

     ...

  Rationale:  This small change was made in the 1668 proposal because 
  the subroutine_call part of the Annex A production is not discussed
  until a later subclause.

. 16.10, p. 347.  In the example "sequence rep_v" at the bottom of the page, 
  the third line

     `true,x = 0 ##0

  needs to be deleted.

. 16.10, p. 348.  Change

     The local variables declared within a sequence or property are
     not visible in the sequence where the sequence or property is
     instantiated.

  to

     The local variables declared within a sequence or property are
     not visible in the context where the sequence or property is
     instantiated.

  Rationale:  The word "context" needs to be used to account for
  both sequence and property instances.  A property cannot be 
  instantiated within a sequence.

. 16.14.7, p. 387, paragraph after "property p".  In the sentence
  beginning "Let t1 be the earliest timestep", the "posedge" in 
  "posedge clk1" should be courier bold in order to be consistent
  with similar phrases.


1668 part 2
-----------

. Annex F.3.2, pp. 1115-1116.  In the grammars for R, S, P, Q, T, and U,
  the font of "e" in 

     ( t v [ = e ]; R )

     ( t v [ = e ]; S )

     ( t v [ = e ]; P )

     ( t v [ = e ]; Q )

     ( t v [ = e ]; T )

     ( t v [ = e ]; U )

  needs to be roman italic, not courier italic.

. Annex F.3.3, p. 1117.  There are several number mismatches due to 
  eliminating explicit discussion of subscripted notations.  Change

     uppercase R denotes an unclocked sequences

  to

     uppercase R denotes an unclocked sequence

  Change

     uppercase S denotes a clocked sequences

  to

     uppercase S denotes a clocked sequence

  Change

     uppercase P denotes an unclocked properties

  to

     uppercase P denotes an unclocked property

. Annex F.3.3, p. 1117.  Change

     Q denotes a clocked property

  to

     uppercase Q denotes a clocked property

. Annex F.3.4.5, p. 1118.  In the last item, the font of "k" in "for k > 1"
  should be roman italic, not courier italic.

. Annex F.5.3, last sentence of first paragraph, p. 1129.  Change

     com pleted

  to
 
     completed

. Annex F.5.3, the second and third "r" in 

     ( t v; \kappa(r) ( ((1, v = e) ##0 (r)) or ((r) intersect 1[*0])) )
  
  need to be in roman italic like the first, not in courier italic.

. Annex F.5.3, the second "r" in 

     ( t v; \kappa(r) ( ((1, v = e) ##0 (r)) )

  needs to be in roman italic like the first, not in courier italic.  Also
  the first "(" after \kappa(r) should be deleted:

     ( t v; \kappa(r) ((1, v = e) ##0 (r)) )

. Annex F.5.3, the second "r" in 


     ( t v; (r) ( ((1, v = e) ##0 (r)) or 1[*0]) )

  needs to be in roman italic like the first, not in courier italic.

. Annex F.5.3, p. 1129, change

     The procedure finishes by applying the function push with hi as
     first argument to each top-level property and descending
     recursively.

  to

     The procedure finishes by applying the function push with <> as
     first argument to each top-level property and descending
     recursively.

. Annex F.5.3, p. 1130.  The second r in 

     push(< >, r ) = r .

  needs to be roman italic like the first.  Also, the reference to
  16.12.6 in the last sentence of this item needs to be changed to 16.13.21.

. I don't think that F.5.2 or F.5.3 should be a part of F.5.  They should 
  be in their own F.x and F.y subclauses.

2175
----

No issue found.


1687
----

. 16.12, third bullet, change

     This is equivalent to ^(<expression>) === 'bx.

  to

     This is equivalent to ^(<expression>) === 1'bx.

  Note that the "1" needs to be added in "1'bx".


1567
----

No issue found.


Annex A
-------

I did not read the whole annex, just the sections with assertion items.

. A.2.10.  In the production for consecutive_repetition, "##[*]" should be
  "[*]" and "##[+]" should be "[+]".