Hi Folks: My notes from today's meeting are attached. Please let me know if changes are required. J.H. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean. Minutes of IEEE P1800 SV-AC meeting #2007-28 Written by: John Havlicek Date: 2007-11-13 Time: 16:00 UTC (10:00 CST) Dialin information: ------------------- Country Number AUSTRALIA 1800009128 AUSTRIA 0800291873 BELGIUM 080077334 CANADA 8008671147 CHINA TELECOM (CT) 108001400732 CHINA NETCOM (CNC) 108007140759 DENMARK 80703159 FINLAND 0800770233 FRANCE 0800941695 GERMANY 08001014519 GREECE 0080016122039738 HONG KONG 800933578 HUNGARY 0680017180 INDIA 0008001006032 INDONESIA 008800105607 IRELAND 1800944116 ISRAEL 1809459738 ITALY 800782388 JAPAN 00531160427 LUXEMBOURG 80023985 MALAYSIA 1800808386 MONACO 80093186 NETHERLANDS 08002658223 NEW ZEALAND 0800443736 NORWAY 80057409 POLAND 008001114672 PORTUGAL 800819106 RUSSIA 81080022801012 SINGAPORE 8001011470 SOUTH AFRICA 0800992835 SOUTH KOREA 00308140540 SPAIN 900967020 SWEDEN 0201400559 SWITZERLAND 0800563054 TAIWAN 00801126585 THAILAND 0018001562039684 UNITED KINGDOM 08005280546 UNITED STATES 8008671147 Access Code: 7375405 Attendance Record: ------------------ 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 New PAR, attendance re-initialized on 2006-08-22: vv[xxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) vv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) nn[---------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) vv[x-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) tt[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) vv[xxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) vv[xxxxxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics) nn[-----------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics) nn[--x------------x--xxx.....................] Joseph Lu (Altera) vv[xxxxxxxxxxxx..............................] Johan Martensson (Jasper) nn[--------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) vv[xxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) vn[x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) vn[x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) vv[x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) vv[xx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |------------------------------------------ attendance on 2007-11-13 |-------------------------------------------- voting eligibility on 2007-11-13 |--------------------------------------------- new voting eligibility Agenda: ------- - Reminder of IEEE patent policy. - Extension period plan (due 2007-11-12) - 1737: Incomplete fix from 1381 . Voice vote on friendly amendments. - 1668: Local variable declaration assignments . Voice vote on revisions based on Champions' feedback. - 1549: Arguments . Voice or e-mail vote on revisions based on Champions feedback - 1648: Default disable iff . Discuss scoping issues. - 1729: Immediate assume, cover [EC] . AI: EC to align with 1641 as described by MK - 2188: Typo in 38.4.1 (occur -> occurs). Major items: - 1932: LTL Operator [DK, DB] - 1900: Checkers [DK] General working items: - 1898: Explicit mappings from assertion system tasks to callbacks [BT] - 2005: Glitches with immediate assertions [ES] - 1995: Assertions and checkers in for loops [ES] - 1756: Control of assertions in initial blocks [EC] . DK: Let's try to write sketches of two possible solutions. - Other items Notes: ------ - Reminder of IEEE patent policy. - Extension period plan (due 2007-11-12) . We sent out our plan for the extension period. . Feedback is welcome, we can make adjustments. . DK will send out the project - 1737: Incomplete fix from 1381 . Voice vote on friendly amendments. . voice vote 0n/0a - 1668: Local variable declaration assignments . Voice vote on revisions based on Champions' feedback. . voice vote 0n/0a - 1549: Arguments . Voice or e-mail vote on revisions based on Champions feedback . reviewed . voice vote 0n/0a - 1648: Default disable iff . Discuss scoping issues. . E.g. if default disable iff is written inside generate, does it apply. . LP will update to make it clearer that default disable iff in nested scope like generate - 1729: Immediate assume, cover [EC] . AI: EC to align with 1641 as described by MK . EC won't get to Dec 1729, 1769, 1758. . JH will review the schedule. - 2188: Typo in 38.4.1 (occur -> occurs). . 0n/0a. Approved by voice. - call for e-mail vote on 1728. Major items: - 1932: LTL Operator [DK, DB] . DB received comments from JM. DB implemented the corrections, but did not post. . DK procedural comment: We should have backup major items. . DB needs to change semantics of clocks, changing clocks. DB needs to implement. - 1900: Checkers [DK] 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? - We agreed that substitution semantics is what we want. 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. - Parameters are passed as arguments. This is like sequences and properties. 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. - DK will recheck. There was a Mantis item in SV-BC, try to use a reference to the general description of name and wildcard binding. 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) - DK we should be consistent with SV-BC way of talking about these ideas. 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"? - JH: I'm not sure that passing @(posedge clk) is illegal, but I don't like this style. 1549 makes clear that passing "posedge clk" to event type is allowed. - DK: We should be consistent. 5. Page 8: Will the "default disable" need to change to "default disable iff"? - DK will 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. - DK: I thought our last decision was to use universal quantification. - ES: Maybe non-deterministic free variables are not ready to be standardized. - TT: We could allow a simulator simply to report failures if the value of a non-deterministc free variable causes failure of an assumption. - DK: Can TT send a suggested rewording. - ES: JH could discuss with Champions their opinion about this and what is reasonable. 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). - DK will change to to use event type argument, and also in other examples. We can revert to untyped if there is a problem with 1549. 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" - DK: There is a mistake here, DK will fix it. 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. - DK: The definition of updating on every timestep is for simplicity. Tools do not have to implement it this way. Freevar updates occur only once. 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. - DK will check and fix as appropriate. 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)" - DK will fix. 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) . . ." - DK 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); YF will send a small example to illustrate the idea behind his third general comment and provide some description of how it is to be interpreted. This is to help facilitate discussion and feedback. We did not get to these items. General working items: - 1898: Explicit mappings from assertion system tasks to callbacks [BT] - 2005: Glitches with immediate assertions [ES] - 1995: Assertions and checkers in for loops [ES] - 1756: Control of assertions in initial blocks [EC] . DK: Let's try to write sketches of two possible solutions. - Other items Next meeting: ------------- 2007-11-20 at 16:00 UTC (10:00 CST), 2 hour slot.Received on Tue Nov 13 18:22:37 2007
This archive was generated by hypermail 2.1.8 : Tue Nov 13 2007 - 18:22:46 PST