List of Mantis items for a Champion's email vote: ------------------------------------------------- 1. 2249 Yes _X_ No ___ Abstain ___ SV-BC 11.4.3.1 merge issue on net and variable types 2. 2233 Yes _X_ No ___ Abstain ___ SV-EC Allowed types for randc 3. 2229 Yes _X_ No ___ Abstain ___ SV-EC Clarify summary description for "inactive" random varaibles. 4. 2183 Yes _X_ No ___ Abstain ___ SV-EC Only simple identifiers allowed in solve-before constraint 5. 2168 Yes _X_ No ___ Abstain ___ SV-AC Formal semantics for edge-sensitive clocks 6. 2150 Yes _X_ No ___ Abstain ___ SV-AC use of automatic variables in action block and subroutine calls should not be allowed Friendly amendments: - "can only be of a type allowed in 16.5.1" --> "shall be of a type allowed in 16.5.1" - "as an argument to subroutine call" --> "as an argument to a subroutine call" - "associate arrays" --> "associative arrays" 7. 2110 Yes ___ No _X_ Abstain ___ SV-AC Allow checkers in procedural for loops Rationale for negative vote: I think that 2088 is changing in response to comments from SV-EC in a way that will not be consistent with the conditional changes on pp. 4-5. In particular, I am concerned about whether a covergroup declaration will be allowed in a checker. Friendly amendments: - Smart quotes should not be used in the courier examples. - In the example beginning at the bottom of p. 2, the sampled value of ok is 1'b1 in the first timestep in which there is a posedge of clk due to the initialization assignment. It is true, although perhaps misleading, to say that the sampled value is always equal to (my_bits[3] == 0). This assumes, of course, that no other code updates my_bits. The declaration of control_variable_copy is not shown, and we do not know what its sampled value is in the first timestep in which there is a posedge of clk. 8. 2106 Yes _X_ No ___ Abstain ___ SV-BC Clarifications needed for declaration before use of objects and type 9. 2091 Yes _X_ No ___ Abstain ___ SV-AC Need a clarification where concurrent assertions may appear Friendly amendments: - Change "in an assertion" to "in a concurrent assertion" in the bullet that begins "Automatic variables and members or elements of". - Change "All variables in an assertion" to "All variables in a concurrent assertion". Rationale for both: 1987 says that "assertion" alone includes both immediate and concurrent assertions. These statements do not apply to immediate assertions. 10. 1987 Yes _X_ No ___ Abstain ___ SV-AC "verification statement" should be italicized and added to the glossary 11. 1932 Yes ___ No _X_ Abstain ___ SV-AC Introduce LTL and other temporal operators Rationale for negative vote: The semantics of "next" described in the clock rewrite rule in F.3.1.2 is not aligned with the semantics of PSL. I strongly believe that it should be aligned. I also have some concern about using the derivations of the derived operators for the definition of the "|=^{non}" relation. Since "|=^{non}" depends on syntax, it may be that the derivations do not give good results. Friendly amendments for non-Annex F: - The paragraph at the bottom of p. 5 and continuing at the top of p. 6 is not consistent with the changes in 1648. I think that there will be no conflict as long as the editor understands that 1932 is not undoing the changes of 1648. - p. 7, change "these operators require parenthesis" to "these operators require parentheses". - p. 7, 16.12.1. In describing the semantics of sequence properties, "sequence_expr" is used in the syntax, but the matching condition is described referring to "sequence". For clarity, I recommend changing strong(sequence_expr) evaluates to true if, and only if, there is a nonempty match of the sequence. to strong(sequence_expr) evaluates to true if, and only if, there is a nonempty match of sequence_expr. and changing weak(sequence_expr) evaluates to true if, and only if, there is no finite prefix that witnesses inability to match the sequence. to weak(sequence_expr) evaluates to true if, and only if, there is no finite prefix that witnesses inability to match sequence_expr. Also, there are many font inconsistencies in this subclause. Hopefully the editor can fix them. - p. 13. 1987 is eliminating "verification statement". I recommend changing "verification statement" to "concurrent assertion" in two places (adjust leading articles as appropriate). I think "concurrent assertion" is the right term because immediate assertions do not have implicit always. Also, the reference to 16.13.4 does not seem to be correct. Should this be to 16.14? Check also in 1987. - p. 15, discussion of p2 and p4. Change "there exist a current or future clock tick" to "there exists a current or future clock tick". - p. 15, discussion of p3. There are font mistakes with "a" and "b" -- they are set in roman and should be courier. - p. 15, 16.12.13. Starting the sentence "The s_eventually property_expr evaluates" is awkward. I recommend deleting "The". - p. 16. Change "there exist a current or future clock tick" to "there exists a current or future clock tick", multiple places. - p. 17, 16.12.15. There are font mistakes with commas in courier bold that should be ordinary roman. - p. 17, 16.12.15, there is a comma splice in last sentence of first paragraph. I recommend changing "are weak, they don't impose" to "are weak: they don't impose". - p. 17, 16.12.16. There are font mistakes with commas in courier bold that should be ordinary roman. - p. 21, 16.13.3. There are font mistakes with commas in courier bold that should be ordinary roman. - p. 21, 16.15.1. m should be in italic in strong(m) and weak(m). b, q, q1, q2 should be in italic in multiple places. Friendly amendments for Annex F: - F.2.3.1, F.2.3.2. The fonts are chaotic and not aligned with the current usage in Annex F. In the derived forms, terminals are set in courier. This includes "(", ")", "[", "]", "1", "+", ":", etc., etc. - F.2.3.2.1, change "when used in a cover or expect verification statement" to "when used in a cover property or expect statement". This is to align with 1987. - F.2.3.2.1, change "when used in an assert or assume verification statement" to "when used in an assert property or assume property statement". This is to align with 1987. - F.3.1.1. The parentheses that are part of the syntax should be in courier. There is a parenthesis mistake in the rule for intersect. first_match requires parentheses around its argument. I think that there are extra parentheses in the [*0] and [*1:$] rules. - F.3.1.2. I think P and Q are interchanged in "produces a property P from a property Q and a clock c". - F.3.3.3. In the rules for "disable iff" and "accept_on", the wrong symbol is used for satisfaction in a number of places. 12. 1830 Yes _X_ No ___ Abstain ___ SV-AC JEITA: A.2.10 There are no Sequence methods(ended, triggered, matched) in the BNF 13. 1827 Yes _X_ No ___ Abstain ___ SV-BC JEITA: 20.3.1 Update the OS Reference 14. 1772 Yes _X_ No ___ Abstain ___ V-1364 inconsistent timecheck/timestamp condition terminology 15. 1769 Yes _X_ No ___ Abstain ___ SV-AC Elaboration time user assertion and error reporting tasks Suggestion: - It is counterintuitive to me that in the example with "module test #(N=12)", the default value of the parameter N is not within the required range from 1 to 8. 16. 1758 Yes _X_ No ___ Abstain ___ SV-AC Boolean implication -> and equivalence <-> 17. 1686 Yes _X_ No ___ Abstain ___ SV-AC assertion evaluation does not wait on subroutines 18. 1447 Yes _X_ No ___ Abstain ___ SV-EC Contradictory stmts about unsized array dimensions (5.1 vs. 5.7 and 5.8) 19. 1340 Yes _X_ No ___ Abstain ___ SV-BC inconsistency between module ports and task arguments 20. 0675 Yes _X_ No ___ Abstain ___ SV-BC Ballot Feedback Issue 203: Packed unions shall not be restricted to equal length items. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Sat Feb 23 13:03:08 2008
This archive was generated by hypermail 2.1.8 : Sat Feb 23 2008 - 13:03:11 PST