Forwarding for Lyes to the full working group. 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:25 ----- Lyes BENALYCHERIF <lyes.benalycheri f@stericsson.com> To Sent by: Dana Fisman <danafi@cs.huji.ac.il>, owner-ieee-1850-i "ieee-1850-issues@server.eda.org" ssues@eda.org <ieee-1850-issues@eda.org>, Sitvanit Ruah/Haifa/IBM@IBMIL cc 10/07/2009 11:51 Lyes BENALYCHERIF <lyes.benalycherif@stericsson.com> Subject RE: comments on the LRM draft Few more. On Section 5.2.1 ¤ p.39 first item b : "V_{i+1}" instead of "V_i+1" (curly brackets missing) ¤ p.40 item f : confusing On Section 5.2.3.2 ¤ p.43 : "nondet() built-in functions" instead of "nondet() or built-in functions" On Section 6.3 ¤ p.99 Example 8 : "([[reg [31:0] i<= 32'd0;]] { [*]; " instead of "{ reg [31:0] i<= 32'd0;[*];" and "|-> {e,f})" instead of "|-> {e,f}" (opening and closing parenthesis missing as well as square brackets for i declaration) Thanks. -- Lyes From: owner-ieee-1850-issues@server.eda.org [owner-ieee-1850-issues@server.eda.org] On Behalf Of Dana Fisman [danafi@cs.huji.ac.il] Sent: Thursday, July 09, 2009 6:19 PM To: ieee-1850-issues@server.eda.org; Sitvanit Ruah Subject: 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 and dangerous content by MailScanner, and is believed to be clean. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.-- This message has been scanned for viruses anddangerous content by MailScanner, and isbelieved to be clean.Received on Sun Jul 12 01:27:18 2009
This archive was generated by hypermail 2.1.8 : Sun Jul 12 2009 - 01:27:20 PDT