Hi Folks: Shalom alerted me that he did not think he copied SV-AC with my Champions ballot, so you can find it attached. I have added some more comments on 1900 as I continue to go through the last 10 pages in detail, so this is not exactly what I sent to the Champions reflector, but that is a minor point. J.H. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean. List of Mantis items for a Champion's email vote: ------------------------------------------------- 1. 2227 Yes _X_ No ___ Abstain ___ SV-EC Incorrect comparison of $random and $urandom 2. 2181 Yes _X_ No ___ Abstain ___ SV-EC Ambiguity in implicit declaration of production variables in randsequence 3 . 1447 Yes _X_ No ___ Abstain ___ SV-EC Contradictory stmts about unsized array dimensions (5.1 vs. 5.7 and 5.8) 4 . 0958 Yes _X_ No ___ Abstain ___ SV-EC dynamic array size method unclear when empty 5 . 1858 Yes _X_ No ___ Abstain ___ SV-EC Name binding in inline constraints 6 . 0520 Yes _X_ No ___ Abstain ___ SV-EC examples of queues assignments are not legal array assignments 7 . 2003 Yes _X_ No ___ Abstain ___ SV-EC Old statement on foreach for wildcard indexed associative arrays 8. 2221 Yes _X_ No ___ Abstain ___ SV-BC "unpacked array reference" is ambiguous No change required. 9. 2193 Yes _X_ No ___ Abstain ___ SV-CC Need to clarify vpiValid flag Duplicate. 10. 2190 Yes _X_ No ___ Abstain ___ SV-CC Standard does not say what should happen when putting value with delay to a dynamic object Duplicate. 11. 2086 Yes _X_ No ___ Abstain ___ SV-CC Deprecated vpiArray still used with vpi_register_cb() description Duplicate. 12. 2063 Yes _X_ No ___ Abstain ___ SV-CC Three minor typos in sections 36.15, 36.21 and 36.25 13. 2016 Yes _X_ No ___ Abstain ___ SV-CC vpiClassType should apply to class typespec rather than to class defn Duplicate. 14. 2009 Yes _X_ No ___ Abstain ___ SV-CC HDL example shown in detail 3 section 36.14 (Reference objects) has errors. 15. 1995 Yes _X_ No ___ Abstain ___ SV-AC Allow concurrent assertions and checkers in for loops Friendly Amendments: - Editorial: I think that the parenthetical exception in the change to 16.4 should be at the end of the sentence. - In the change to 16.14.3, I'm not sure that shall count each possible set of loop control variable values as one attempt is really clear. Based on the sentence that follows, I think that what is intended is something like shall count distinct valuations of loop control variable values as separate attempts - Editorial: At the bottom of p. 2, the comma following the bold courier "continue" should be in non-bold roman. - Editorial: Do not use smart quotes in the courier examples. - p. 3, change "generated" to "executed" in "the pass action block will be generated". - p. 4. In the example above, ac1 will always be checking the sampled value of variable ok. Since this will be equal to (my_bits[3] == 0) by the end of any time step, it will always pass The declaration and initialization of "ok" are not shown, so we do not know its sampled value in timesteps prior to and including the first timestep in which posedge clk occurs. Similar comments apply to other statements in this paragraph. 16. 1952 Yes _X_ No ___ Abstain ___ SV-CC "Null argument" to mean "omitted argument" may be confusing 17. 1846 Yes _X_ No ___ Abstain ___ SV-BC D3 21.13: add 1800-2008 to `begin_keywords No change required (subsumed). 18. 1826 Yes _X_ No ___ Abstain ___ SV-BC JEITA: Annex B Add keyword list by LRM version 19. 1741 Yes _X_ No ___ Abstain ___ SV-CC 1800-2005 Section 27.50 Issues with foreach diagram 20. 1729 Yes _X_ No ___ Abstain ___ SV-AC Introduce immediate assume and cover statements 21. 1728 Yes _X_ No ___ Abstain ___ SV-AC Introduce "let"statement Friendly Amendment: - p. 3, I think that there is a parenthesis mismatch (too many ")") in the let in the package pex_gen9_common_expressions. 22. 1711 Yes _X_ No ___ Abstain ___ SV-BC Rules for unique case evaluation Duplicate. 23. 1668 Yes _X_ No ___ Abstain ___ SV-AC Local variable initializers. 24. 1667 Yes _X_ No ___ Abstain ___ SV-AC Local variable arguments for sequences and properties. 25. 1549 Yes _X_ No ___ Abstain ___ SV-AC add missing formal argument types 26. 1456 Yes _X_ No ___ Abstain ___ SV-CC Clarify, circumscribe restrictions on use of DPI context utilities 27. 0748 Yes _X_ No ___ Abstain ___ SV-CC vpiParent of var select can only be array var 28. 1900 Yes ___ No ___ Abstain _X_ SV-AC Add new 'checker' construct to SVA Rationale for Abstain: I collected too many friendly amendments below to justify a clear "Yes" vote, and I'm still going carefully though the last 10 pages of the proposal. Friendly Amendments: - 16.18.1, p. 8. I'm not sure that the following sentence is precise enough to interpret what "remains valid" means: If the fact that the abstract model is indeed an abstraction of a concrete model can be formally proven then the reasoning about the abstract model behavior remains valid for the behavior of the concrete model. Presumably, there is a correspondence between the behaviors. In any case, I don't think this statement is needed in the LRM. - 16.18.2, p. 11. In If a formal argument is written in the checker body, its corresponding actual argument shall be a checker variable or a formal argument in another checker. I recommend changing "formal argument is written" to "formal argument is assigned a value". This is for consistency with the other sentences in this paragraph. - 16.18.4, p. 14. There is a type mismatch in the example with check_in_context. The formal argument enable is of type logic, but the instance my_check1 binds to it the sequence expression "en1 ##1 en2". One solution is to change the actual to something like "en1 || en2" and also change the parenthetical clause: note also that a sequence has been passed to the checker as its enabling condition Alternatively, the type of the formal argument should be changed. - 16.18.5, p. 16. The following sentence As regular variables, checker variables can be packed or unpacked aggregates of other types (see 6.5). should be reworded for clarity. The phrase "as regular variables" could be omitted entirely or changed to something like "as in the case of regular variables". - Editorial: 16.18.5, p. 16. Change "show" to "shows" in "The following example show". - 16.18.6, pp. 16-17. The intuitive descriptions of the assumptions imposed on the free checkvar bit flag seem reasonable for a formal tool in which $global_clock ticks at every point in time. In simulation, however, $global_clock may not be at the granularity of a timestep and a simulator may apply chaotic values for flag in timesteps that are not ticks of $global_clock. In this situation, the intuitive descriptions do not seem accurate. I recommend either 1. Stating that it is assumed that $global_clock ticks at every timestep, or 2. Qualifying the intuitive descriptions in a way that makes it clear that they apply only in the timesteps in which $global_clock ticks. - 16.18.6, p. 18. If a simulator cannot assign a right value needs to be reworded to clarify what "assign a right value" is intended to mean. - 16.18.6, p. 18. which in turn implies that the corresponding legality of data transfer through that transaction is being checked. The legality might not be checked in simulation because the simlator might choose the wrong value for mem_data. I think this sentence needs to be worded in a way that does not suggest that checking of legality is ensured in simulation. - Editorial: p. 19. Change "as opposite to" to "as opposed to". - 16.18.6.1, p. 19. In Example 1, the constant "3'b3" should be something like "3'd3" or "3'h3". Similarly with "3'b5". - 16.18.6.1, p. 20. I would change "the clock of the sequence" to "the ending clock of the sequence" in In nonblocking assignments the matched method provides synchronization between the clock of the sequence I would also change "when the sequence clock" to "when the ending clock of the sequence" in the sentence that follows (2 places). In the examples that follow, the second "endsequence : s1" should be "endsequence : s2". Also, we don't really have enough information to conclude the following: On the contrary, the value of u at time 90 will be 0 since there is no match of s2 at time 90. This statement assumes that there is not another match of s2 ending at 90. - 16.18.6.1, p. 20. I recommend deleting "Thus," from Thus, an unpacked structure or array can have one element assigned procedurally and another element assigned continuously. This conclusion does not follow from the preceding. Also, "can" should probably be "may". - 16.18.6.1, p. 21. I'm not sure how the SAR is interpreted when the check bit to be assigned may be determined dynamically. In Example 4, the discussion says that there is a SAR violation for counter[0]. Is this just because i may take the value 0? Is the following legal free checkvar bit [5:0] counter; free checkvar bit [1:0] i; assign counter [5:4] = foo; always_check @clk counter[i] <= !counter[i]; ? - 16.18.6.4, p. 26. The shifting of the NBA when future value functions appear in the RHS may produce counterintuitive results in simulation if the $global_clock is not the fastest. - Editorial: 16.18.6.4, p. 26. At the bottom of the page there is an extraneous ",". - Editorial: 16.18.6.4, bottom of p. 27. Remove "an" in "One such an order is".Received on Tue Feb 5 07:46:55 2008
This archive was generated by hypermail 2.1.8 : Tue Feb 05 2008 - 07:47:09 PST