Hi Folks: We had ballots close on 1898 (failed), 2171 (passed), 1900 (failed), and 1533 (failed). See the results below. J.H. ---------------------------------------------------------------------------------- Ballot on Mantis 1898 - Called on 2007-11-06, final ballots due by 2007-11-13 T 23:59-08:00. yv[xxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) yv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) n[--------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) yv[-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) yv[xxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) nv[xxxxxxx-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) v[xxxxxxxxxxx..............................] Johan Martensson (Jasper) n[-------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) yv[xx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) n[-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) n[-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) yv[-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) v[x-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |----------------------------------------- attendance on 2007-11-06 |------------------------------------------- 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 [MK] I vote 'no' because this document does not seem to be aligned to draft4. In the last part it says: "Annex M, change the following on page 1107". But Annex M does not have that line number. ---------------------------------------------------------------------------------- Friendly Amendments [DK] Fix fonts on page 2 (subclauses 38.4.2 and 38.5.1): E.g., cbAssertionEnableFailAction should be in Times Roman Bold ---------------------------------------------------------------------------------- Ballot on Mantis 2171 - Called on 2007-11-06, final ballots due by 2007-11-13 T 23:59-08:00. yv[xxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) yv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) n[--------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) yv[-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) yv[xxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) v[xxxxxxx-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) v[xxxxxxxxxxx..............................] Johan Martensson (Jasper) n[-------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) yv[xx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) yn[-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) n[-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) yv[-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) yv[x-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |----------------------------------------- attendance on 2007-11-06 |------------------------------------------- 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 ---------------------------------------------------------------------------------- Ballot on Mantis 1900 - Called on 2007-11-06, final ballots due by 2007-11-13 T 23:59-08:00. v[xxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) yv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) n[--------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) v[-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) v[xxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) v[xxxxxxx-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) v[xxxxxxxxxxx..............................] Johan Martensson (Jasper) n[-------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) v[xx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) yn[-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) n[-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) yv[-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) nv[x-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |----------------------------------------- attendance on 2007-11-06 |------------------------------------------- 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 [TT] 1. Page 7: "When a checker is instantiated . . ." Are we sure that we want to continue using substitution semantics for the checker construct? Maybe an instantiation semantics would be easier to define? 2. Page 2: "Parameters for checkers and properties" OK, I at least see one reason for using substitution semantics. It at least allows the checker to handle variations in signal width or type. However, beyond that, it will be impossible to write a flexible checker without some support for parameters. We'll be forced to use modules for any checker that requires parameters to set options for the checker. 3. Page 7: "An implicit .* port connection . . ." This paragraph spends too much time explaining the difference betweeen .name and .* port connections. That is explained elsewhere. This paragraph needs to concentrate on the interaction between the port connection method and default values on the formal argument. For example, a default value will never be used if the argument is connected with .name. Also, on the bullet points directly above, we could clarify as follows: -- Named port connection using implicit connections (.name syntax) -- Named port connection using a wildcard port name (.* syntax) 4. Page 8: When connecting a clock of a checker, what is the proper syntax? my_check check_inside (a, posedge clk); or my_check check_inside (a, @posedge clk); and why? Is it currently allowed to connect a port to "posedge clk"? 5. Page 8: Will the "default disable" need to change to "default disable iff"? 6. Page 12: "Note that although the behavior . . ." I thought we had decided not to specify the effect of assume property statements on free variable values. 7. Page 16: Example 1: What is the proper type for a checker clock? Here it's defined as "bit", just like any other signal. However, it's being passed an event (@posedge clk). 8. Page 16: Example 2: "In this example fv1[0] is assigned . . ." "In the assignment of fv2 the sampled value of fv1[0] is sampled since fv1[0] is a continuous free bit and the value of fv1[1] is not sampled since fv1[1] is a sequential free bit" This seems backward from the paragraph above: "All variables participating in the right-hand side of a free variable assignment are sampled, except the continuous free bits" 9. Page 16: Didn't we decide to drop continuous assignments to free variables at one point? It seems they add a lot of complexity to the proposal. 10. Page 17: 16.18.5.2 "the value of b in the assertion is sampled while the value of c is not" Again, this is backwards with respect to the paragraph cited above. 11. Page 20: "Then $sampled(v) returns v.$past(v,1,en, clk) This needs to change for clarity: "Then $sampled(v) returns v. The expression $past(v,1,en, clk)" 12. Page 20: "The future value of v $future_gclk(v)" This also needs to change for clarity add a comma to separate v from the expression that follows. If that doesn't visually separate them enough we may have to rewrite further: "The future value of v, given by $future_gclk(v) . . ." 13. Page 20: "The equivalent form after rewriting is . . ." In the re-written form, a does not change if b changes: only if c changes. To account for that, an extra term has to be added "assign a = $changed_gclk($past_gclk(b)) || $changed_gclk(c) ? $past_gclk(b) && c : $past_gclk_(a); ---------------------------------------------------------------------------------- Friendly Amendments [BT] - 25.2 Packages may ("may" should be in blue) - 36.9 Checkers VPI diagram: vpiDefaultDisable should point to a distribution not just an expr. [YF] General syntax (in the beginning and end of the document) * The proposal should change module_or_interface_or_generate_item otherwise the BNF of generate_region,loop_generate_construct can't reach checker_or_generate_item_declaration (need to put restrictions such that checker items can only be used in checkers like done for interface vs. module). * better to include clocking_declaration in the checker items o.w it would only be possible to declare the clocking outside and use it by hierarchical path (if this is possible) since currently only "default clocking clocking_identifier" is allowed (making all the examples illegal...) * adjust default disable to what is approved. * what about let_declaration (as in 1728) in checker_items? * checker_instantiation ::=3D checker_identifier name_of_instance ([list_of_port_connections]) ; Whereas list_of_port_connections allows only to pass expression. This would disallow passing sequence and property expressions. * page 8: it is mentioned: "Variables used in a checker that are neither formal arguments to the checker nor internal variables of the checker are resolved according to the scoping rules from the scope in which the checker is declared." Don't you mean where the checker is *instantiated* instead of declared ? o.w how does this apply to all the examples with "property defined_elsewhere" ?=20 * page 22: "While procedural statements (if, case, ...) cannot be placed directly in checkers .." - where is that said ? Doe's this mean the following code is illegal ? Why ? freevar r; always_check @(posedge clk or negedge rst_b) if (!rst_b) r <=3D 1'b0; else ... * page 22: "generate if (coverage_level !=3D ovl_cover_none) begin cover_b" - missing colon after the named block cover_b * mentioned in example page 9 that you can instantiate a checker inside a procedural statement, should be in the syntax somewhere (statement_item) *general notes: * if in a checker only always_check and initial_check are allowed and outside checker those are not allowed then why not simply have always and initial inside checker ? ,after all we don't have always_interface or initial_program . I understand there are different context infer rules but those can be made if you are inside a checker or not. * page 9 + later: we were trying to get rid of untyped arguments so I think it is better to give examples with typed arguments when possible (or use the untyped keyword) * having freevar being deterministic is counterintuitive to me, can we have freevar and regular vars inside checkers where freevar are those not being assigned (and thus free) ? This is similar to the current formal verification tools behavior I'm familiar with (where anything undriven (net or reg) is "x" or "free") ---------------------------------------------------------------------------------- Ballot on Mantis 1533 - Called on 2007-11-07, final ballots due by 2007-11-14 T 23:59-08:00. yv[xxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) yv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) n[--------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) v[-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) v[xxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) v[xxxxxxx-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) v[xxxxxxxxxxx..............................] Johan Martensson (Jasper) n[-------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) yv[xx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) n[-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) n[-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) v[-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) v[x-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |----------------------------------------- attendance on 2007-11-06 |------------------------------------------- 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 -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Thu Nov 15 12:50:19 2007
This archive was generated by hypermail 2.1.8 : Thu Nov 15 2007 - 12:50:29 PST