Resending ... seems to be stuck in the reflector 1932 Review 2007-10-16 ---------------------- * Throughout. Check font sizes. I think the LRM uses 10 pt Roman font and 9 pt Courier font. This may not be necessary. * Throughout. Review and revise for standard English. * In Syntax 16-14, the parentheses terminals need to be in bold red. For "strong" and "weak", they are in red, but not bold. The parentheses for property_expr, if...else, accept_on, reject_on are neither red nor bold. * p. 5. Keywords cited in text (e.g., if...else, next) should be in bold Courier. They are bold Roman. * p. 6. Compare operator precedence with PSL. I am concerned that all the temporal operators are at the same precedence. * p. 6. I'm not sure accept_on, reject_on should be left associative. Maybe they shouldn't have an associativity because they have only one property argument. They also are not infix. Also always, eventually. ??? Compare with PSL. * p. 5 and p. 6 (two places). The formatting of the paragraph beginning "A disable iff clause can be attached" needs to be aligned with Draft4. There is a display line for "disable iff (expression_or_dist) property_expr". * p. 7. 16.12.1. I think that the semantics of sequence properties should first be described carefully in a manner similar to the descriptions of the other property forms. Those descriptions talk about attempts and are more precise than this description. (More comments below.) * p. 7. 16.12.1. In the forms "strong(sequence_expr)", etc., sequence_expr should not be in italic. It should be upright Courier. When sequence_expr is referenced in the text (not within a coded expression), then it should be in italic Roman. * p. 7. 16.12.1. I recommend putting the sentence forbidding sequences that admit empty match right after the first sentence that describes the three forms. I don't think we should define semantics for empty match, and this should be clear. Also, this sentence needs to make clear that it applies to sequence_expr within "strong" and "weak". The description of the semantics of "weak(sequence_expr)" is not accurate. It does not account for something like "1[*0:$] ##1 0". I think that the sentence "In other words" should not be phrased this way. It seems that it is a restatement of the restriction that sequence_expr not admit empty match. I am confused about the scope of In other words it is evaluated false if, and only if there is a finite prefix of the computation, which witness that there is no nonempty match of the sequence. Failure of "strong(sequence_expr)" is not accurately described by this sentence. This sounds more like the semantics of weak(sequence_expr). I don't think "computation" is generally used in Clause 16, so I recommend finding a different way to talk about this. Look for cues in other parts of Clause 16. * p. 7. 16.12.1. I think depends on the statements in which should be depends on the verification statement in which Also, use "verification statement" rather than just "statement" thereafter. * p. 8. 16.12.1. I think that "property p2 is meaningless" should be rephrased. The property has a meaning. The LRM should say what the meaning is. The LRM can comment on its usefulness, but I would avoid that. I would just say what it means. I would rephrase the description of c1 and a1 to be parallel. E.g., The cover property c1 says that clk must rise at least once and that a is true when clk rises for the first time. The assertion a1 says that if clk rises at least once, then a must be true when clk rises for the first time. Note that the last sentence here ends with a comma instead of a period in the proposal. * p. 8. 16.12.2. "not" should be bold Courier in "The not operator switch[es] the strength. "Strength of a property" has not been defined in general. The LRM will probably be able to talk more clearly about strength of an operator than strength of a property. In the examples, the keywords should be in bold Courier. Consider whether to use different labels on the two assertions, since they are not equivalent. * p. 8. 16.12.2. The first property_expr is in italic Courier. It should be in italic Roman. * p. 9. I don't understand the Note to editor: Insert the subclause "16.12.2 Implication" here (as 16.12.6) that appears before 16.12.7. * p. 9. 16.12.7. I think that "implies" should be capitalized as the first word of the subsubclause title, even though it is a keyword. * p. 9. 16.12.7. I would not write the sentence When property_expr1 and property_expr2 are boolean, then property_expr1 implies property_expr2 is similar to property_expr1 -> property_expr2. without further explanation. This sentence could be omitted. If you want to illustrate the similarity I recommend saying more precisely what is alike and what is not alike. Similar comments for iff and <->. * p. 9. 16.12.8. Check for dependencies on 1549. The references to property_expr and property_spec should be in italic Roman. * p. 9. 16.12.9. There is an inconsistency between the use of followed_by and followed-by in the text. * p. 9. 16.12.9. I think that you need to say that sequence_expr is the antecedent and property_expr is the consequent in sequence_expr #-# property_expr sequence_expr #=# property_expr I recommend that you follow very closely the form of the text in the current 16.12.2 for this subsubclause. I think that doing so will enable the reader to discern more easily the difference between these and the dual |->, |=>. * p. 10. 16.12.9. The description for example p2 could be written more clearly. I recommend changing Property p1 says that done shall be asserted at some clock tick during first 6 clock ticks, and starting from one of the clock ticks when done was asserted rst shall always be low. Property p2 says that done shall be asserted at some clock tick during first 6 cycles, and starting from one of the clock tick following the clock tick when done was asserted rst shall always be low. to Property p1 says that done shall be asserted at some clock tick during the first 6 clock ticks, and starting from one of the clock ticks when done is asserted, rst shall always be low. Property p2 says that done shall be asserted at some clock tick during the first 6 clock ticks, and starting the clock tick after one of the clock ticks when done is asserted, rst shall always be low. * p. 10. 16.12.9. I think the equivalence between followed_by and concatenation for sequences is useful. Does this include non-vacuity? * p. 10. 16.12.10. The fonts are not consistent for the keywords. They should be bold Courier. * p. 10. 16.12.10. Avoid labels like "weak form with range". Instead, create a unique phrase that can be used throughout the LRM to refer to this operator form. E.g., "weak ranged next operator". By the way, shouldn't this be "iterated weak next operator" instead? The ranged forms involve also the quantifier (forall, exists). Similar comments apply to strong next. The description of the semantics of the iterated weak next operator needs to be made more precise. Refer to the non-terminal constant_expression. I recommend considering defining the semantics of next operators as deriveds: next p \equiv 1 |=> p next[n] p \equiv 1[*n] |=> p s_next p \equiv 1 #=# p s_next[n] p \equiv 1[*n] #=# p If this is satisfactory, it will be crisper. I expect that considering this will help to determine how non-vacuity and clock change rules should be defined for next. This proposal doesn't seem to talk about multiclock support for the LTL operators. There will be issues if the multiclock rules are not relaxed. One would expect #-# to have the same restrictions as |->. From the forms above, it seems that clock change after next should be allowed. I am not happy with the presentation of the examples. I prefer to change the long list of examples into pairs of related examples and intersperse the relevant text. This will make it easier for the reader to see the similarities and differences in the related pairs and it reduces the eyestrain from jumping around the page. I think that the intuitive description of the semantics of next needs to say something about what "next" means with respect to the beginning of an evaluation attempt. Is the next clock tick always strictly after the beginning of the attempt of the next property? I think some phrase should be chose to describe this and that phrase should be used consistently in talking about the examples. Currently, the description of the examples uses phrases like "the property clock ticks once more", "a shall be true at each future clock tick starting from the next clock tick", "if the property clock ticks at least once", etc. // Did not review after 16.12.10. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Tue Oct 16 12:28:09 2007
This archive was generated by hypermail 2.1.8 : Tue Oct 16 2007 - 12:28:15 PDT