[$ieee-1850] Fw: comments on the LRM draft - from Dana

Sitvanit Ruah
Formal Verification Group
IBM Haifa Research Laboratory
Tel:  972-4-828-1249

----- Forwarded by Sitvanit Ruah/Haifa/IBM on 12/07/2009 11:24 -----
                                                                           
             Dana Fisman                                                   
             <danafi@cs.huji.a                                             
             c.il>                                                      To 
             Sent by:                  ieee-1850-issues@eda.org, Sitvanit  
             dana.fisman@gmail         Ruah/Haifa/IBM@IBMIL                
             .com                                                       cc 
                                                                           
                                                                   Subject 
             09/07/2009 19:19          comments on the LRM draft           
                                                                           
                                                                           
                                                                           
                                                                           
                                                                           
                                                                           




Sitvanit, all,

Please find below some comments on the LRM draft.

   Comments on Section 5.2.1:

   1. Section 5.2.1, p.39: there are undrerscors that were meant to
      indicate subscripts. That is V_{k-1} should be capital V with
      subscript ‘k-1’. This should be fixed all over the section.
   2. Section 5.2.1, p.39: the hyphen in “The meaning of the HDL expression
      is determined with respect to a given verification unit which acts as
      the root of a verification run - the root verification unit.” is
      shorter than it should be.
   3. Section 5.2.1, p.39, first “b)” item: the word “inherit” should
      appear in bold font as in the item c).
   4. Section 5.2.1 uses the term “inheritance graph” which is only defined
      in Section 7. I suggest to add a parenthetical note pointing to the
      page where inheritance graph is defined. Also, consider moving the
      definition from Section 7 to the definitions section.

   Comments on Section 6.3:

   5. Section 6.3, p.96: The sentence “A local variable can be referenced
      by any Boolean expression in which it is visible, and it can be
      referenced by or modified by any procedural block in which it is
      visible.” is a bit hard to parse as the part about a “local variable
      can be referenced by” repeats itself. I suggest breaking and
      rephrasing it as follows: “A local variable can be referenced by any
      Boolean expression or procedural block in which it is visible.  A
      local variable can be modified by any procedural block in which it is
      visible.”
   6. Section 6.3, p.97, below Figure 4: The use of the term “time” is
      inadequate. It should be “cycle” (or “evaluation cycle”).
   7. Section 6.3, p.97: bad opening quotes in ”multiple independent
      copies” and in ”will be born”.
   8. Section 6.3, p.98, Example 6: bad opening quotes in ”frees”.

   Comments on Section 6.4:

   9. Section 6.4, p.99-100, Restrictions: The font of the restrictions is
      too big.
   10.      Section 6.4, p.99, 2nd restriction: The first sentence seems to
      be missing the word “it” after “should be such that” and before “can
      be inserted into …”.
   11.      Section 6.4, p.99, 2nd restriction: bad opening quotes in
      ”shell”.
   12.      Section 6.4, p.100, Example 9: In the definitions of A1 and A2
      a quote appears as ‘0’. That is the definitions should be corrected
      to:
A1 : lv<= 32`d0;
      A2 : lv<=lv + 32`d1;
   13.      Section 6.4, p.102, Example 10: In the definitions of A1,A2 and
      A3 a quote appears as ‘0’. That is the definitions should be
      corrected to:
A1 = lv <= 32`d0;
A2 = lv <= lv + 32`d1;
A3 = lv <= lv + 32`d1;

   Comments on Section 6.5:


   14.      Section 6.5, p.107, NOTES: The font of the notes is too big.

   Comments on Section 7:

   16.      Section 7.1.2, p.116: The first sentence of this section should
      be corrected to: “The Assume Directive, shown in Syntax 7-87,
      instructs the verification tool to constrain the verification (e.g.,
      the behavior of the input signals) so that the given property holds.”
      That is, instead of “a property” it should be “the given property”.
   17.      Section 7.1.4, p.118: Table 6 is textually crowded. The text in
      each of the columns should start some space after the line marking
      the beginning of the column. The first and second columns can be made
      a bit more narrower without causing line breaks.
   18.      Section 7.1.4, p.119: Table 7 is textually crowded. The text in
      each of the columns should start some space after the line marking
      the beginning of the column. The first column should be made a bit
      wider so that lines would not break.
   19.      Section 7.2.4.1., p.129, first paragraph: The word “sig1”
      should be in system font (at least 4 occurrences).
   20.      Section 7.2.4.2., p.129: The hyphen in the sentence starting
      “If signal sig1 is a design signal of design mydesign,” should be
      longer.
   21.      Section 7.2.4.2., p.129-130: The word “sig1” should be in
      system font (at least 3 occurrences).
   22.      Section 7.2.4.3., p.130-131: The word “sig1” should be in
      system font (at least 6 occurrences).
   23.      p.132-138: too many blank pages.

   Dana-- This message has been scanned for viruses anddangerous content by MailScanner, and isbelieved to be clean.