Hi Doron: Please find below my comments on the 1932 proposal document for changes outside Annex F. Now I need to move on to the Annex F document. Best regards, John H. -------------------------------------------------------------- 1932 Review: JH Notes 2008-01-06 --------------------------------- * p. 2, changes to Syntax 16-14. I don't understand the coloring conventions. I think that in the production options that are not being changed, the syntax terminals should still be in bold red. E.g., parentheses in "( property_expr )" and "not" in "not property_expr". Please check for similar inconsistencies in the changes for A.2.10. * p. 3, end of changes to Syntax 16-14. Again, I don't think that the coloring conventions are being followed. However, these trailing productions are not being changed, so they could be deleted. * p. 5. There is something missing form the sentence. I think change Properties may be built from other properties or sequences using instantiation, and the described in the following subclauses. to Properties may be built from other properties or sequences using instantiation and the operators described in the following subclauses. * p. 6. There is something wrong with the coloring in the sentence describing Table 16-25. The sentence about omitting precedence for strong and weak sequences must be new, so it should be in blue. Also, I think that it should be changed from The precedence for strong and weak sequences is not defined because these sequences use parenthesis. to The precedence for the strong and weak sequence operators is not defined because these operators require parenthesis. * p. 6., Table 16-25. "Not" should be "not"; "iff" should be bold. // Sanity examples for operator precedence. // // property prop_weak_until(property p,q); // q or p and next prop_weak_until(p,q); // endproperty // // property prop_weak_until(property p,q); // next prop_weak_until(p,q) and p or q; // endproperty // // r |-> next(p and q) % parentheses required // r |-> next(p until q) % parentheses required // r |-> p and next q // r |-> (next q) and p // r |-> next(s |-> p) % parentheses required * p. 6, Table 16-25. Consider lowering the precedence of "next" family. Perhaps it could go between "|->" and "always"? REMARK: I have gone back through some of the mail on operator precedence. I'm not sure that it is good to rely on deeper operand analysis as a part of parsing to resolve precedence conflicts. I don't think we have done this in past discussions of similar operator relationships. For example, I saw Johan's comments that interpreting next r |-> p as (next r) |-> p is not possible because of syntax error. But I would read this instead as saying that if "next" is higher precedence than "|->", then parentheses are required to avoid syntax error: next(r |-> p) // legal next r |-> p // syntax error, since this groups as (next r) |-> p This is similar to a ##1 (b throughout c[->1]) // legal a ##1 b throughout c[->1] // syntax error * p. 6, Table 16-25. Consider lowering the precedence of "iff". I'm not sure where the logical implication operators are going, but maybe "iff" should be with them. My guess is that these should be lower precedence than "|->". My rationale has to do with the way we interpret operator precedence with respect to syntax as described above. * p. 7, 16.12.1. Change "sequence property" to "sequential property". The English is better formed this way. * p. 7, 16.12.1. I think that the font of "sequence_expr" should be changed from courier or courier italic to roman italic. I don't like the disconnect between "sequence_expr" in the first three sentences and "sequence" in the last sentence. I recommend changing A sequence that admits an empty match is not allowed as a property. to The sequence_expr of a sequential property shall not admit an empty match. * p. 7, 16.12.1, intuitive description of semantics of weak(sequence_expr). I didn't follow all the discussion on this, but I think the phrase there is no finite prefix that witnesses a non-match of the sequence should be changed to something like there is no finite prefix that witnesses inability to match the sequence My rationale is that a directintuitive interpretation of the phrase "prefix that witnesses a non-match" is "a prefix over which there is not a match", but this is not the meaning that we want. * p. 7, 16.12.1, minor English editing for grammar and clarity. Change Without the strong, weak operators, the evaluation of sequence_expr depends on the verification statements in which it is being used. In case that the statement is assert property or assume property, it is evaluated as weak(sequence_expr), otherwise it is being evaluated as strong(sequence_expr). to If the strong or weak operator is omitted, then the evaluation of the sequence_expr depends on the verification statement in which it is used. If the verification statement is assert property or assume property, then the sequence_expr is evaluated as weak(sequence_expr). Otherwise, the sequence_expr is evaluated as strong(sequence_expr). * p. 7, 16.12.1 and elsewhere. Change property is evaluated to <logic value> to property evaluates to <logic value> We use the latter form many other places in the LRM. I also think this turn of phrase is more common in English (e.g., "expression evaluates to <value>" rather than "expression is evaluated to <value>"). * p. 7, 16.12.1. However, the explanation for that is more complex. I don't like this. I think we should try to refine the text suggested by Johan. I would rewrite Note that a poperty of the form weak(sequence_expr) is evaluated to true if and only if the property weak(first_match(sequence_expr)) is evaluated to true. However, the explanation for that is more complex. as something like Similarly, a property of the form weak(sequence_expr) evaluates to true if and only if the property weak(first_match(sequence_expr)) evaluates to true. This is because a prefix witnesses inability to match sequence_expr if, and only if, it witnesses inability to match first_match(sequence_expr). * p. 8, 16.12.1. I recommend rewriting 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. One problem with this is that the notion of evaluation attempt is not included. We define the result of an evaluation attempt of the top-level property of a verification statement to be true or false or disabled or etc. We also say that an evaluation attempt of the top-level property of a verification statement begins at each occurrence of the leading clocking event for that statement. Since the evaluation attempt doesn't even exist without the occurrence of the clocking event, I don't think that the difference between weak and strong sequential property can be well illustrated by single-cycle sequences within assertion directives. It is true that in Annex F we define satisfaction of an assertion directive whose top-level property is clocked by looking at each suffix of the word, but this notion is not well correlated with the concept of evaluation attempt (e.g., it doesn't lead to a useful notion of the number of attempts in a simulation). Also, the global view of the result of evaluation of an assertion directive involves combining the results of the various evaluation attempts, a notion that is also absent from the description in the proposal. I think that this discussion will be clearer if we focus on a single evaluation attempt and avoid highlighting the initial clock tick of the evaluation attempt. Perhaps: property p3; b ##1 c; endproperty c1: cover property (@(posedge clk) a #-# p3); a1: assert property (@(posedge clk) a |-> p3); ... The sequential property p3 is interpreted as strong in the cover property c1. An evaluation attempt of c1 returns true if, and only if, a is true at the tick of posedge clk at which the attempt begins and both of the following conditions are satisfied: - b is true at the tick of posedge clk at which the attempt begins. - There exists a subsequent tick of posedge clk and c is true at the first such tick. The sequential property p3 is interpreted as weak in the assert property a1. An evaluation attempt of a1 returns true if, and only if, either a is false at the tick of posedge clk at which the attempt begins or both of the following conditions are satisfied: - b is true at the tick of posedge clk at which the attempt begins. - If there exists a subsequent tick of posedge clk, then c is true at the first such tick. * p. 8, 16.12.1. I am confused by Since the sequential property a ##1 b is used in an assertion, it is weak. This means that at the last cycle of a simulation the sequential property a ##1 b always holds and thus, the assertion a1 always fails. Does "last cycle of a simulation" mean "last timestep" or "last occurrence of the clocking event <for this assertion>"? If the clocking event for the assertion happens to occur in the last timestep of the simulation, then these two notions coincide, but even in that case, I'm not sure that the statement above is accurate -- if a is not true in that timestep, then it is not the case that the assertion fails. I recommend rewriting this as Since the sequential property a ##1 b is used in an assertion, it is weak. This means that if a holds at the last tick of the assertion's clock in a simulation, the weak sequential property a ##1 b will also hold beginning at that tick, and so the assertion a1 will fail. * p. 9, note to editor before 16.12.7. I think that this should read Note to editor: Insert the subclause entitled "Implication" (16.12.2 in Draft 4) here as 16.12.6. Rationale: There is no subclause entitled "Implication subclause". * p. 9, semantics of "iff". I know what the semantics of "iff" is, but if I didn't I might find it hard to find where the implicit parentheses are in A property of this form evaluates to true if and only if either property_expr1 evaluates to false and property_expr2 evaluates to false or property_expr1 evaluates to true and property_expr2 evaluates to true. I recomend a minor change to something like A property of this form evaluates to true if and only if either both property_expr1 and property_expr2 evaluate to false or both property_expr1 and property_expr2 evaluate to true. * p. 9, 16.12.9, followed_by. I don't think "specifies that there should be" is correct LRM-ese usage of "should". I recommend changing to "shall". * p. 10, 16.12.9. My interpretation of operator precedence is that not sequence_expr |-> not property_expr is a syntax error, and similarly with |=>. I recommend adding parentheses: not(sequence_expr |-> not property_expr) and similarly. * p. 10, 16.12.9, bottom of the page. I have been dinged for using "Note that". I think that there are IEEE rules about what is a note and people don't like it if you use the turn of phrase "note that" when you are not describing an IEEE note. I don't think that IEEE notes are normative, so it is probably best to avoid the word "note", even though this style is commen in written mathematics. One might just delete "Note that". Also, there is a stray period before "Note". * p. 10, 16.12.9, minor English editing to improve number agreement. I recommend changing The followed_by operators are especially convenient for specifying cover properties over sequences followed by a property. to A followed_by operator is especially convenient for specifying a cover property directive over a sequence followed by a property. * p. 11, 16.12.10, description of various forms of "next". In the parenthesized phrases, such as "weak next operator", I do not think that "next" should be in a special font. It looks bold to me. In these contexts, I think that "next" is a single word in a multi-word technical phrase that is being defined. In any case, the bolding of "next" does not seem to be consistent across the four forms. * p. 11, 16.12.10. I recommend making the intuitive descriptions of the semantics tied more directly to the non-terminals referenced in the syntax. This style is used in a number of the other subclauses for property forms. I recommend changing Weak next property evaluates to true if property_expr holds at the next clock tick or if there are no further clock ticks. To require the clock tick to occur, use the strong form s_next property_expr. Weak next property with const_expression evaluates to true if property_expr holds in the specified of future clock ticks indicated by the const_expression, or if there are not enough clock ticks for the property to complete the evaluation. To require the necessary clock ticks to occur use the strong form s_next [const_expression] property_expr. to The weak next property next property_expr evaluates to true if, and only if, either there property_expr evaluates to true beginning at the next clock tick or there is no further clock tick. The strong next property s_next property_expr evaluates to true if, and only if, there exists a next clock tick and property_expr evaluates to true beginning at that clock tick. The indexed weak next property next [ const_expression ] property_expr evaluates to true if, and only if, either there are not const_expression clock ticks or property_expr evaluates true beginning at the last of the next const_expression clock ticks. The indexed strong next property s_next [ const_expression ] property_expr evaluates to true if, and only if, there exist const_expression clock ticks and property_expr evaluates true beginning at the last of the next const_expression clock ticks. Making these bullets or interleaving them into the preceding bullets may be clearer. * p. 11, 16.12.10, "note". Similar remark about using the phrase "Note that" and IEEE notes. Maybe it is best to delete "Note that", i.e. change Note that next property_expr is semantically equivalent to 1 |=> property_expr, and that s_next property_expr is semantically equivalent to 1 #=# property_expr. to next property_expr is semantically equivalent to 1 |=> property_expr, and s_next property_expr is semantically equivalent to 1 #=# property_expr. * p. 11, 16.12.10. There is inconsistent use of bold font in s_eventually in the declarations of properties p5 and p6. * p. 12, 16.12.10, intuitive semantics of the examples. I think that the phrases used for the various examples should be more consistent. For example, the descriptions of p1 and p2 use phrases like "property clock ticks once more" in talking about next and s_next, while the description of p5 uses the phrase "property clock ticks at least once". I think that "at least once more" is more accurate than "at least once". Consider an evaluation attempt that starts on a tick of the clock. The tick of the clock at the start of the attempt does not count as the next tick. The subtleties are more problematic when the attempt does not start on a tick of the clock. A resonable solution may be only to describe single clock semantics here and align the phrases used to describe the additional clock ticks. Maybe the following phrases are good: next // "next clock tick", "first future clock tick" next[k] // "kth future clock tick" The additional subtleties should be described somewhere, probably in a section on multiclock next (which may exist later -- I haven't looked ahead). * p. 12, 16.12.10. There is something missing from the sentence The property p6 says that should be true sometime in the strict future. Probably this should be something like The property p6 says that a shall be true at some strictly future clock tick. * p. 12, 16.12.10. I recommend changing The properties p7 and p8 say that a shall be true the second clock ticks to The properties p7 and p8 say that a shall be true at the second future clock tick * p. 12, 16.12.11. I think Note that the only strong form of always operator is with a bounded range. should be The strong form of always operator is allowed only with a bounded range. * p. 12, 16.12.11. I think that the description of the always operators can be made clearer. I find confusing the discussion of whether clock ticks exist because it is not stated clearly whether these clock ticks are for the ranges or for the evaluation of the underlying property_expr: or if there are not enough clock ticks for the property to complete the evaluation I think the intention is that they refer to the ranges, since the evaluation of the underlying property_expr should follow its own structure. I recommend changing A property always property_expr evaluates to true if property_expr holds at every clock tick. A property always [cycle_delay_const_range_expression] property_expr evaluates to true if property_expr holds at every clock tick within the range of future clock ticks, or if there are not enough clock ticks for the property to complete the evaluation. To require the necessary clock ticks to occur use the strong form s_always [constant_range] property_expr. to A property always property_expr evaluates to true if, and only if, property_expr holds at every current or future clock tick. A property always [cycle_delay_const_range_expression] property_expr evaluates to true if, and only if, property_expr holds at every current or future clock tick that is within the range of clock ticks specified by cycle_delay_const_range_expression. It is not required that all clock ticks within this range exist. A property s_always [constant_range] property_expr evaluates to true if, and only if, all current or future clock ticks specified by constant_range exist and property_expr holds at each of these clock ticks. * p. 12, 16.12.11, rewording for clarity. I recommend changing In that case the verification statement will evaluate the underlying property_expr starting at every occurrence of its leading clocking event, unless the verification statement is placed inside an initial block. The implicit always in the following example will succeed in every attempt, if and only if the explicit always will succeed in its single attempt: Implicit form: assert property (p); Explicit form: initial assert property (always p); to A verification statement that is not placed inside an initial block specifies that an evaluation attempt of its top-level property shall begin at each occurrence of its leading clocking event. In the following two examples, there is a one-to-one correspondence between the evaluation attempts of p specified by the implicit always from the verification statement implicit_always and the evaluation attempts of p specified by the explicit always operator in excplicit_always: Implicit form: implicit_always: assert property (p); Explicit form: initial explicit_always: assert property (always p); * p. 13, 16.12.11, example a1 is missing a ")" before ";". Also, the non-overlapping #=# should be used because otherwise there is a conflict between reset and !reset. * p. 13, 16.12.11. Change The assertion a1 says that reset shell to The assumption says that reset shall Rationale: "shell" is a misspelling. I think "assumption" makes more sense because "assume property" is written in the example. * p. 13, 16.12.11. Change The assertion is being evaluated once starting at the first clock tick to The assumption is evaluated once starting at the first clock tick. Note the addition of the period at the end. * p. 13, 16.12.11. For clarity, I recommend changing The property p1 says that if there is a followed by b then starting from the next clock tick after b c shall be forever true. to The property p1 says that if a is true at the first clock tick and b is true at the second clock tick, then c shall be true at every clock tick that follows the second. * p. 13, 16.12.11. For clarity, I recommend changing The properties p2 and p3 say that during the clock ticks 2, 3, 4, and 5 a shall be true. The difference between them is that p3 requires the property clock to tick at least 5 more times. to The properties p2 and p3 say that a shall be true at each of the second through fifth clock ticks after the starting clock tick of the evaluation attempt. Property p3 requires that these clock ticks exist, while property p2 does not. * p. 13, 16.12.11. For clarity, I recommend changing The property p4 is true if a remains true starting from the second clock tick (the clock is not required to tick). to The property p4 evaluates to true if, and only if, a is true at every clock tick that is at least two clock ticks after the starting clock tick of the evaluation attempt. These clock ticks are not required to exist. * p. 13, 16.12.12. For minor English editing and clarity, I recommend changing An until property of the non-overlapping form evaluates to true if property_expr1 evaluates to true at every clock tick until at least one tick before a clock tick where property_expr2 evaluates to true. The overlapping form evaluates to true if property_expr1 evaluates to true at every clock tick until and including a clock tick at which property_expr2 evaluates to true. The strong forms of an until property require that property_expr2 eventually happens in the future (this also include the requirement from the property clock to tick enough times), while the weak forms evaluate to true even if property_expr2 never happens provided that property_expr1 is always true at each clock tick. to An until property of one of the non-overlapping forms evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 evaluates to true. An until property of one of the overlapping forms evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until and including a clock tick at which property_expr2 evaluates to true. An until property of one of the strong forms requires that a current or future clock tick exist at which property_expr2 evaluates to true, while an until property of one of the weak forms does not make this requirement. An until property of one of the weak forms evaluates to true if property_expr1 evaluates to true at each clock tick, even if property_expr2 never holds. * p. 14, 16.12.12. For clarity, I recommend changing The property p1 says that a remains true until (not including) b becomes true. If b never becomes true a shall remain true forever. to The property p1 says that a shall be true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until, but not including, a clock tick at which b is true. If there is no current or future clock tick at which b is true, than a shall be true at every current or future clock tick. If b is true at the starting clock tick of the evaluation attempt, then a need not be true at that clock tick. * p. 14, 16.12.12. For clarity, I recommend changing The property p2 says that a remains true until (not including) b becomes true, and that b shall eventually happen. to The property p2 says that there shall exist a current or future clock tick at which b is true and that a shall be true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until, but not including, the clock tick at which b is true. If b is true at the starting clock tick of the evaluation attempt, then a need not be true at that clock tick. * p. 14, 16.12.12. For clarity, I recommend changing The property p3 says that a remains true until (including) b becomes true. If b never becomes true a shall remain true forever. to The property p3 says that a shall be true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until and including a clock tick at which b is true. If there is no current or future clock tick at which b is true, than a shall be true at every current or future clock tick. * p. 14, 16.12.12. For clarity, I recommend changing The property p4 says that a remains true until (including) b becomes true, and that b shall eventually happen. to The property p2 says that there shall exist a current or future clock tick at which b is true and that a shall be true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until and including the clock tick at which b is true. * p. 14, 16.12.12. Copy-paste error. Change The property p2 is equivalent to strong(a[*1:$] ##0 b). to The property p4 is equivalent to strong(a[*1:$] ##0 b). * p. 14, 16.12.13. Change one of the following forms form to one of the following forms: * p. 14, 16.12.13. I think Note that the only weak form of eventually operator is with bounded range. should be The weak form of eventually operator is allowed only with a bounded range. * p. 14, 16.12.13. For clarity, I recommend changing The s_eventuality property evaluates to true if property_expr evaluates to true in a finite number of clock ticks, and the clock shall tick enough times for property_expr to happen. to The propert s_eventually property_expr evaluates to true if, and only if, there exists a current or future clock tick at which property_expr evaluates to true. Note that "s_eventuality" is changed to "s_eventually". Also, check the bold font consistency. The "s_" in "s_eventually" should be bold. * p. 14, 16.12.13. For clarity, I recommend changing Weak eventually property with range evaluates to true if property_expr holds somewhere within the range of future clock ticks indicated by the constants, or if there are not enough clock ticks for the property to complete the evaluation. to The ranged weak eventually property eventually [constant_range] property_expr evaluates to true if, and only if, either there exists a current or future clock tick within the range specified by constant_range at which property_expr evaluates to true or not all the current or future clock ticks within the range specified by constant_range exist. Rationale: I really don't think that the phrase "there are not enough clock ticks for the property to complete the evaluation" makes it clear that "not enough clock ticks" applies only to the clock ticks specified by constant_range. * p. 14, 16.12.13. For clarity, I recommend changing To require the necessary clock ticks to occur use the strong form s_eventually [constant_range] property_expr. The constant_range may be unbounded for the strong form, but shall be bounded for the weak form. to The ranged strong eventually property s_eventually [cycle_delay_const_range_expression] property_expr evaluates to true if, and only if, there exists a current or future clock tick within the range specified by cycle_delay_const_range_expression at which property_expr evalutes to true. The range for a strong eventually may be unbounded, but the range for a weak eventually shall be bounded. Rationale: For the change to the second sentence, constant_range is not used in the syntax for the strong form. * p. 14, 16.12.13, in the declarations of p1, p2, and p3 change eventually to s_eventually Rationale: eventually requires a range, and the strong form is implied by the English descriptions of p1 and p2. * p. 15, 16.12.13. For clarity, I recommend changing The property p1 says that a shall happen some time in the future. It is equivalent to ##[*0:$] a. to The property p1 says that there shall exist a current or future clock tick at which a is true. It is equivalent to strong(##[*0:$] a). * p. 15, 16.12.13. For clarity, I recommend changing The property p2 says that starting from some point on a should be always true. to The property p2 says that there shall exist a current or future clock tick such that a is true both at that clock tick and also at every subsequent clock tick. * p. 15, 16.12.13. For clarity, I recommend changing The property p3 says that for infinite computations a shall becomes true infinitely many times, and for finite words, a should hold at the last clock tick. to For a computation with infinitely many clock ticks, the property p3 says that a shall be true at infinitely many of those clock ticks. For a computation with finitely many clock ticks, the property p3 says that if there is at least one clock tick, then a shall hold at the last clock tick. * p. 15, 16.12.13. For clarity, I recommend changing The properties p4 and p5 say that a shall be true at some tick between the second and the fifth clock ticks; p4 does not require the clock to tick, while p5 does. P4 is equivalent to weak(##[2:5] a), and p5 is equivalent to strong(##[2:5] a). to The property p4 says that if the second through fifth clock ticks from the starting clock tick of the evaluation attempt all exist, then a shall be true at one of these clock ticks. p4 is equivalent to weak(##[2:5] a). The property p5 says that there shall exist a clock tick at which a is true and that is between the second and fifth clock ticks, inclusive, from the starting clock tick of the evaluation attempt. p5 is equivalent to strong(##[2:5] a). * p. 15, 16.12.13. For clarity, I recommend changing The property p7 says that the clock shall tick enough times and a shall happen in the future, to The property p7 says that there shall exist a clock tick at which a is true and that is no earlier than the second clock tick after the starting clock tick of the evaluation attempt. * p. 15, 16.12.15. I don't think that the statement a failure of the property s_eventually a cannot be identified in a finite time: if it is violated, the value of a must be always false. is accurate for computations with finitely many clock ticks (in particular, for finite computations). I recommend changing E.g., the property always a is safety since it is violated only if at some (finite) time a becomes false. To the contrary, a failure of the property s_eventually a cannot be identified in a finite time: if it is violated, the value of a must be always false. to E.g., the property always a is safety since it is violated only if after finitely many clock ticks there is a clock tick at which a is false, even if there are infinitely many clock ticks in the computation. To the contrary, a failure of the property s_eventually a on a computation with infinitely many clock ticks cannot be identified at a finite time: if it is violated, the value of a must be false at each of the infinitely many clock ticks. * p. 16, 16.13.2. The ")" in "(not, and, or)" should be in roman, not courier bold font. The "(" and "," and ")" in "(accept_on, reject_on)" should be in roman, not courier bold font. * p. 17, 16.13.2. In the first sentence of the rewritten text, there are six occurrences of "," in bold courier font that should be roman. * p. 17, 16.13.2, first sentence. There is a problem because the sentence refers specifically to the operators "next", "always", "until", and "eventually", when in fact all the operators in the associated families (e.g., next, s_next, and the ranged versions, etc.) are presumably meant. I think that there needs to be a solution that makes clear the difference between reference to a specific operator and reference to the family. In other places in the LRM, regular roman font has been used to refer to families (e.g., case). It may be best to try to include in each section on a family of operators a specific statement about which operators are in the family and how the family will be referenced in the future. * pp. 17-18, 16.13.2. For clarity, I recommend changing The temporal operators next, always, until, and eventually require their operands to occur in future cycles. The exact timing where they should hold is determined according to the leading clock of the underlying property. Therefore, the operands properties shall begin on the same clock as the clock of the underlying property. to Each of the temporal operators <in the next, always, until, and eventually families> specifies evaluation of its underlying operand properties at current and future ticks of clock incoming to the temporal operator. Therefore the leading clock of each underlying operand property shall be the same as the clock incoming to the temporal operator. I have used "<>" to indicate that I'm not sure what the exact solution will be for referencing families of temporal operators (e.g. next family). * p. 18, 16.13.2. Change but @(posedge clk0) (@(posedge clk1)s1 until @(posedge clk0) s2) is illegal because the (@(posedge clk1)s1 operand property begins on a different clock from the clock of the underlying property to but @(posedge clk0) ( (@(posedge clk1) s1) until @(posedge clk0) s2) is illegal because the leading clock of the operand property @(posedge clk1) s1 is different from the clock incoming to the until operator. I added parentheses around "@(posedge clk1) s1" because I don't think it is clear @(posedge clk0) is the clock incoming to the until operator in the original. I think the clock flow rules should say that for @(c) (@(d)p until q), @(c) first flows into the parenthes, so this should be the same as (@(c) @(d) p until q) and then @(c) should be overridden by @(d), which leaves us with (@(d) p until q) and in this form, @(d) should apply to the until. There could still be a conflict with the leading clock of q, as above. * p. 18. I think that there need to be some updates to 16.13.3 on clock flow to clarify how the new temporal operators behave. The existing principles should be preserved, but some turns of phrase currently in 16.13.3 may be misleading in the presence of the new operators. I think that these principles include the following: . a clock does not flow through another clock . a clock flows from left to right through an expression (sequence or property) . a clock flows into and across parenthesized subexpressions . a clock does not flow out of enclosing parentheses What is not so clear is how the clock flow interacts with the parsing resolution of operands, which may involve introducing implicit parentheses. We may need to work out some more formal representation of the clock flow. We have not defined @(c) as an operator, so we need to say, in a case like @(c) ( @(d) p until q ) whether @(c) or @(d) is the clock incoming to "until". * p. 18, 16.15.1. Please check for font chaos in this section and try to follow the fonts conventions already in use. The operands in the definition of semantic leading clock are set in roman italic, not courier, courier italic, courier bold, or courier bold italic. * p. 18, 16.15.1. I guess that it is o.k. that the semantic leading clock definition does not include all operators from the various families since the current definition is not complete for all operators. * p. 20. Please remedy the font chaos. Check for "," set in courier (bold?) that should be in roman in the first sentence of the replacement text. Also there is the problem of referencing the families of operators. Also check for font inconsistencies as described in previous bullets. Note that roman italic, not courier italic, is currently used in the LRM for the operands in general statement (not examples, though). Also, subscripting in the existing LRM has not been respected. Probably, "m |-> q (m #-# q)" should be "m |-> q (respectively, m #-# q)" and similarly in a number of places. * p. 20, the last "And" of part a) should not be capitalized. * p. 21, part b). Please align the fonts with corrections as indicated above. Also check for incorrect bold courier. Check for bold period after "is not". * p. 21, part c). I think that there are some open technical considerations concerning the determinization of the incoming outer clock to an "until" and how this interacts with clocks in the left operand. As I've suggested above, I think that in @(c) (@(d) p until q) (where p, q do not have clocking events), the incoming clock to the until should be @(d), not @(c). * p. 21, part d). Change The cycle where the evaluation of q should start are being determined by c; to The cycle in which the evaluation of q starts is a clock tick of c; * p. 21, part e). Change The cycles where the evaluation of q should start are being determined by c; to The cycles at which evaluations of q start are clock ticks of c; * p. 22, part f). Change The cycles where the evaluation of q should start are being determined by c; to The cycle at which evaluation of q starts is a clock tick of c; * p. 22, 36.45. The changes are not correctly colored. * I am a bit disturbed that we don't have a simple syntax for a strict nexttime that synchronizes between two clocks, e.g. so that @(c) a |=> @(d) b could be written also as @(c) a |-> <weak synchronizing strict nexttime> @(d) b It may not be important to try to achieve this in the 2008 standard. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Sun Jan 6 18:26:07 2008
This archive was generated by hypermail 2.1.8 : Sun Jan 06 2008 - 18:26:51 PST