Failed. See below. J.H. --------------------------------------------------------------------------------- BALLOT on Mantis 1932 - Called on 2008-01-15, final ballots due by 2008-01-28 T 23:59-08:00. yv[xxxxxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) v[xxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) n[----------------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) yv[xxxxxxxx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) t[xxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) yv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) v[xxxxx-xxxxxxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics) n[------------------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics) n[---------x------------x--xxx.....................] Joseph Lu (Altera) yv[xxxxxxxxxxxxxxxxxxx..............................] Johan Martensson (Jasper) n[---------------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) yv[xxxxx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) yv[xxxxxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) n[-------x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) nv[xxxxxx-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) v[xxxxxxxxx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |------------------------------------------------- attendance on 2008-01-15 |--------------------------------------------------- voting eligibility for this ballot |---------------------------------------------------- email ballots received Legend: x = attended - = missed r = represented . = not yet a member v = valid voter (2 out of last 3 or 3/4 overall) n = not a valid voter t = chair eligible to vote only to make or break a tie ---------------------------------------------------------------------------------- Rationale for Negative Vote [BT] ** I think the proposal has some important additions e.g. strong/weak qualifiers, followed by (visual notation of followed by needs improvement). However, the additional syntax, particularly where it goes far into s_... variants for example instead of finding a way to compose qualifiers/directives should not become part of the language keywords. Rather we should leverage libraries and keep the syntax simple and minimal where possible to keep SVA simple and highly approachable. In fact, recent/in-the-works constructs and facilities like checkers and macros make such an approach more palatable. I vote no in hopes that we can find a way to remedy (at least some of) these. ---------------------------------------------------------------------------------- Friendly Amendments [BT] ** Minor fix: The second vpiOverlapImplyOp should be a vpiOverlapFollowedByOp. [YF] 1. add to "36.45 Property specification" and "M.2 Source code" vpi codes for weak,iff,implies=20 2. in 16.13.3 Clock flow -=20 "flows left to right across linear operators (e.g., repetition, concatenation, negation, implication, and the next,always, eventually operators) and distributes "... I would also add the "followed by" (though it is only an example),also maybe saying it flows left to right in implication operator is a bit misleading since "implies" is not linear 3. in 16.15.1 - if this definition correlates to the abstract grammar then I think definition for the weak and strong operators is missing (whereas always , eventually and reject_on operators are redundant since those are derived but that is OK) 4. This enhancement adds additional operand types to property expression,e.g: the cycle_delay_const_range_expression in=20 always [cycle_delay_const_range_expression] property_expr , currently only property-expression or sequence-expression operands exist in property-expression, are those additional operand types accessible from the VPI ? (I'm sorry but I don't know enough about VPI to answer this...) [DK] LTL_Formal.080115.pdf Page 11. "is implicitly *define* by unrolling *their* derivation" -> "is implicitly defined by unrolling their derivation" LTL.1932.080123.pdf General note. It looks like all the fonts are too small. E.g., the normal text is in New Times Roman 8 instead of 10. =20 * Page 2. The assertion examples in the motivation section should be in black. * Page 3, second line "s_eventually", "s_" should be in bold. * Page 7. "Since only one match of a sequence_expr needed for strong(sequence_expr) to hold, a poperty of the form strong(sequence_expr) evaluates to true if and only if the property strong(first_match(sequence_expr)) evaluates to true. * "one match of a sequence_expr": "sequence_expr" should be in italic. * "for "strong(sequence_expr)"" : "()" should not be bold * "poperty" -> "property". * "true" should not be italicized. * Page 7. "...and c is true..." c should not be bold. * Page 8. Assertions a1 and a2. ##1 should not be bold. * Page 8. "The not operator switches ..." need a reference to 16.12.2. * Page 8. "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. In this case it is more reasonable to use:" * Need to introduce a clock, say @clk in these examples. * I prefer the explanation which would cover both simulation and formal verification: "This means that if clk stops ticking and a holds at the last tick of clk, the weak sequential property a ##1 b will also hold beginning at that tick, and so the assertion a1 will fail. In this case it is more reasonable to use:" * Page 9. "A property is a followed_by if it has one of the following forms...". followed_by should be in regular italic (actually, I am not quite confident, followed_by is a name like implication, and implication is rendered in regular Times New Roman. One is clear, it shouldn't be courier. Whatever you choose, be consistent throughout the document: either use regular or italic Times New Roman.) * Page 9. Syntax diagram: #-# and #=3D# should be in red. * Page 9. Make uniform spacing between bullets. * Page 10. "Therefore, sequence_expr #=3D# property_expr is equivalent to the following: sequence_expr ##1 1 #-# property_expr". I don't think that these formulas are equivalent. The equivalent form after clock rewriting is sequence_expr ##1 @11 #-# property_expr, but this cannot be written in the body of LRM. I would drop this rewriting note. * Page 10. "sequence_expr #-# strong(sequence_expr1)". "#-#" should not be in bold. * Page 11. First line: "(indexed form of weak next )" --> : "(indexed form of weak next)" - Drop a space. * Page 11. "either there are not const_expression clock ticks or property_expr evaluates true" --> "to true". * Page 11. "only if, there exist const_expression clock ticks and property_expr evaluates true" --> "to true". * Page 12. "A property is an always if it has one of the following forms, which use the always operators:". "always should be in courier 9. Check all other occurrences of this and other operators (until, etc.). * Page 13. "Implicit_always: assert property(p);" --> "implicit_always". * Page 13. "initial explicit_always: assert property(always p);" "explicit_always" should not be in bold. * Page 14. "clock tick exist at which property_expr2". property_expr2 should be in regular courier 9 (same regarding next occurrences of property_expr1 and property_expr2). * Page 14. s_until and s_until_with in the examples should be in bold. * Page 14. "and that a shall be true": a should be in courier 9. * Page 14, at the bottom. "(ranged weak form of eventually)" should be in Times New Roman. * Page 15, at the top. Same comment about "(ranged weak form of eventually)". * Page 15, examples. All occurrences of "s_eventually" should be in bold (sometimes only "eventually" is in bold). * Page 16. Delete "h)". * Page 20. "intersection, if-else, and the until": "and" should be in Times New Roman. * Page 24. Note the list item numeration in the WITH clause * Page 25. 4). Insert values for accept_on and reject_on from 1751. Also in M.2 (page 26). * Page 25 #-# and #=3D# should not be in bold. [LP] 1. Editorials in blue: For example, consider the following assertion: a1: assert property (@clk not a ##1 b); Since the sequential property a ##1 b is used in an assertion, it is weak. This means that if clk stops ticking ... =20 2. Two forms of followed-by are provided: Overlapped using operator #-# and nonoverlapped using operator #=3D#. (The line spacing is weird here. It looks like there is an extra return after operator) =20 3. initial explicit_always: assert property(always p); The bold is bsckwards (keywords area not bold and should be). The previous examples need to be fixed also. Similarly, in subsequent examples, should s_always and s_next should be bold too. =20 4. this is more of a question. I have become confused on the meaning of followed-by. Should I be thinking along the lines of attempts, or is this a one time thing as though it is in an initial block? I understood the description and examples, but not the equivalency expressions to |-> and |=3D>. I am having trouble following what happens at a specific = clock tick when the sequence on the LHS is false - does that attempt pass or fail? There is something missing here.=20 =20 5. shouldn't examples p2 to p5 in the description of always have the ##[range] instead of range?. property p3; s_always [2:5] a; endproperty =20 should be=20 =20 property p3; s_always ##[2:5] a; endproperty =20 I think this: =20 s_always [constant_range] property_expr (ranged strong form of s_always) =20 should be: =20 s_always ##[constant_range] property_expr (ranged strong form of s_always) =20 I think it will be very strange if always uses the ## and s_always does not which is what the current syntax shows. In any case the examples here are inconsistent with the syntax. The same issue exists with eventually. =20 6. s_until and until_with, etc should be bold =20 7. didn't Dmitry's 1683 change this: the "clock for the end of the antecedent must be the same as the clock for the beginning of the consequent." =20 =20 8. I would like to discuss whether recursive support is necessary at this time. =20 9. I would to understand whether this is dependent on the proposal for the VPI changes, or whether this could get accepted without the VPI getting accepted. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Tue Jan 29 06:38:29 2008
This archive was generated by hypermail 2.1.8 : Tue Jan 29 2008 - 06:38:40 PST