Hi Folks: My notes from yesterday's meeting were rather chaotic, and I tried to add some details about some of the technical discussions before sending them out. Also, we have several proposals that could be voted this week if revised in a timely manner. Each proposal owner should give me clear indication of whether such a proposal is ready for vote no later than today 2008-01-23 18:00 -0600 Let me know if other 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-36 Written by: John Havlicek Date: 2008-01-22 Time: 16:00 UTC (10:00 CST) Dialin information: ------------------- Toll number: +1 647 723 3904 Country Toll Free 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[xxxxxxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) vv[xxxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) nn[-----------------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) vv[xxxxxxxxx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) tt[xxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) vv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) vv[xxxxxx-xxxxxxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics) nn[x-------------------------------------------------] Ah-Lam Lee (Qualcomm) nn[-------------------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics) nn[----------x------------x--xxx.....................] Joseph Lu (Altera) vv[-xxxxxxxxxxxxxxxxxxx..............................] Johan Martensson (Jasper) nn[----------------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) vv[xxxxxx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) vv[xxxxxxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) nn[--------x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) vv[-xxxxxx-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) vv[xxxxxxxxxx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |-------------------------------------------------- attendance on 2008-01-22 |---------------------------------------------------- voting eligibility on 2008-01-22 |----------------------------------------------------- new voting eligibility Agenda: ------- - Reminder of IEEE patent policy. Champions results (recent meeting 2008-01-17): - 1648 - 1682 - 1683 - 1668 - 1987 Ballot results - 1769 - 1900 - 2005 - 2088 - 2089 - 2150 - 2182 Ongoing ballots: - 1932: LTL Operators [DK, DB] Old items: - 1503 has been returned to SV-AC from SV-CC. - 1995: Assertions and checkers in for loops [ES]. - 2005: Glitches with immediate assertions [ES]. Comments from Tej Singh. - 2091: Clarify where concurrent assertions may appear [LP]. [Did JH fail to call vote?] Major items: - 2005: review - 2110: review General working items: - 1901: Identifier for ## should be constant [EC] . Need reviewers. - 1769: Elaboration-time assertions and error reporting [EC] Other items Notes: ------ - Reminder of IEEE patent policy. Champions results (recent meeting 2008-01-17): - 1648: Sent back to SV-AC for revision, then to SV-CC . LP will try to get rid of the "local" and "locally". . JH & LP will revise, then we will call for an email vote. - 1682: Sent to SV-CC to review callbacks and approve. . JH will move this to SV-CC and send mail to Charles Dawson. - 1683: Approved by Champions. - 1668: Not discussed. . JH will open a new mantis item for VPI changes for 1668. - 1987: Sent back to SV-AC for revision. . Stu did not like "verification statement". . Shalom objected to the sentence "When an assertion is a statement that something must be true..." . Should expect be a verification statement? . We will take this to e-mail to figure out what to do. Ballot results - 1769: Passed with friendly amendments. . EC will revise to address LPs comments. . JH recommended that we ask Shalom how to write the sentence involving "may not". . EC will revise to put the new material in Clause 19. JH will call for an email vote. - 1900: Passed, no friendly amendments. . There were comments by MK and DK revised the proposal during the ballot period. . Voice vote to approve the changes: 8y/0n/0a. . JH will move to resolved. - 2005: Passed with friendly amendments. . ES will revise. . Discussion about $assertoff. Suppose $assertoff is executed in a timestep in which there has already been one or more evaluations of a deferred assertion. - LP suggested that if the deferred assertion had executed at least once in the timestep, then it should be allowed to continue executing in that time step, even after the $assertoff. This was in analogy with concurrent assertions, for which an attempt that is already started will not be stopped by a $assertoff. The intuition is that the multiple executions, maturation, and flushing are a way of getting the effect of the deferred evaluation. - ES argued that $assertoff should prevent all subsequent evaluations, and any previous evaluations would be left in the queue. This rule is simpler and aligns with immediate assertions. - It was agreed that intermingling $assertoff with iterations of a deferred assertion in a single timestep is inherently problematic. - JH comment added to the notes after the meeting: I tend to agree with LP's intuition that the multiple iterations are a mechanism for defining a single deferred evaluation. It seems that the simpler definition does not give a useful capability when the $assertoff is intermingled with iterations of the assertion in a single timestep, so one should be sure that this is the desired tradeoff. . Discussion about counters. - There is a tradeoff of tool efficiency for usefulness of a capability. - Reporting deterministic success counts in the typical use case adds queueing overhead that is trying to be avoided. - JH said that if the counts are not deterministic, then they will likely not be useful anyway. What is it that is really of use? ES said that users will want to know whether an assertion was executed at all. JH suggested getting rid of the counter specification and writing a less restrictive requirement that the tool provide the information that the user desires without saying exactly how. - 2088: Failed due to negative vote. . Discussion of sample, ended vs. triggered - MK expressed concern about stating equivalence of ended and triggered in checkers. Triggered seems like the - JH asked why it is important to have both? - DK argued that ended is natural in checkers because the execution is in the Observed region. . Send comments to Tom by 2008-01-25. We did not have time to discuss the technical issues in the following failed votes: - 2089: Failed due to negative votes. - 2150: Failed due to negative vote. The owners of these items should follow up to understand how to address the negative feedback and friendly amendments. We did not have time to discuss the technical issues in the following failed vote, but it was indicated that all comments have been addressed already: - 2182: Failed due to negative votes. . JH will call for a new vote. Ongoing ballots: - 1932: LTL Operators [DK, DB] . JH reminded the committee of the ongoing ballot closing 2008-01-28. Other items - 1698: . EC reviewed and had comments. LP revised, but EC has not re-reviewed. . EC will re-review, and JH will call for a vote if the proposal is ready. - 2168: . There have been comments. - DK has three proposals ready to review. JH asked DK to send mail to solicit reviewers for those proposals. We did not have time to discuss the following: Old items: - 1503 has been returned to SV-AC from SV-CC. - 1995: Assertions and checkers in for loops [ES]. - 2005: Glitches with immediate assertions [ES]. Comments from Tej Singh. - 2091: Clarify where concurrent assertions may appear [LP]. [Did JH fail to call vote?] Major items: - 2005: review - 2110: review General working items: - 1901: Identifier for ## should be constant [EC] . Need reviewers. - 1769: Elaboration-time assertions and error reporting [EC] ------------------------------------------------------------------------- Remaining Extension Schedule Legend: M: major item slot (2 concurrent) m: minor item slot (4 concurrnet) v: very minor item slot (no limit) d: draft preparation slot (no limit) Items returned from Committees: ------------------------------- 1503 // SV-CC [LP,BT are monitoring] Items in other Committees: -------------------------- 1599 // SV-CC [BT is monitoring] 1601 // SV-EC 1757 // SV-CC 1758 // SV-BC 1898 // SV-CC Late Items: ----------- m: 1756 // due 2007-12-11; review M: 1932 // due 2007-11-27; review M: 1900 // due 2007-12-04; ballot & revision m: 1729 // due 2007-12-18; ballot & revision v: 1786 // due 2007-12-18; resolve in 1932 v: 1687 // due 2008-01-15; open m: 2172 // draft due 2007-12-18 d: 2173 // draft due 2008-01-08 d: 2069 // draft due 2008-01-15 Schedule: --------- 2008-01-15 M: 1667 ballot & revision M: 2005 review m: 2172 ballot & revision m: 2150 ballot & revision m: m: 1769 ballot & revision v: 1687 ballot & revision v: 1901 review d: 0966/1982 draft d: 2110 draft d: 2069 draft d: 1987 draft 2008-01-22 M: 2005 review M: 2110 review m: 2173 review m: 2150 ballot & revision m: 1769 ballot & revision m: 2069 review v: 1901 ballot & revision v: 1987 review d: 0966/1982 draft d: 2100 draft d: 1686 draft d: 1830 draft 2008-01-29 M: 2005 ballot & revision M: 2110 ballot & revision m: 2173 ballot & revision m: 0966/1982 review m: 2100 review m: 2069 review v: 1686 review v: 1830 review v: 1987 ballot & revision d: 1806 draft 2008-02-05 M: 2005 ballot & revision M: 2110 ballot & revision m: 2173 ballot & revision m: 0966/1982 ballot & revision m: 2100 ballot & revision m: 1806 review v: 1686 ballot & revision v: 1830 ballot & revision 2008-02-12 M: 2069 ballot & revision M: 1551 review m: 0966/1982 ballot & revision m: 2100 ballot & revision m: 2168 review m: 1806 review 2008-02-19 M: 2069 ballot & revision M: 1551 ballot & revision m: 2168 ballot & revision m: 1806 ballot & revision m: m: 2008-02-26 M: 1551 ballot & revision M: m: m: m: m: ================================================================== OLD Notes: ------ - Reminder of IEEE patent policy. Champions results - Upcoming meeting 2008-01-17. . The following SV-AC items are on the agenda: 1648, 1682, 1987, 1683, 1668. Ballot results - 1667: Local variable arguments [JH]. . Voice vote to change "cannot" to "shall not" 7y/0n/0a. . We will create a separate mantis for the VPI. - 1729: Immediate assume and cover [EC]. . EC will revise to put in the page break from BT's friendly amendment. Ongoing ballots: - 1900: Checkers [DK]. . LP will send a ballot in later today. . If there are no negative votes, JH will send mail to Neil Korpusik about Champions proactively starting consideration of 1900. . DK will address any friendly amendments on 2008-01-16 or, at latest, 2008-01-17, and JH will call for e-mail vote to approve friendly amendments closing 2008-01-21. - 2091: Clarify where concurrent assertions may appear [LP]. . LP has addressed the technical points in the negative votes. . If there are no further change requests from the current ballot, JH will call for another e-mail vote to end 2008-01-21. Old items: - 1995: Assertions and checkers in for loops [ES]. . Voice vote to approve ES's implementation of the rewording changes suggested by Shalom Bresticker. 9y/0n/0a . JH will mark as resolved. - 2005: Glitches with immediate assertions [ES]. Comments from Tej Singh. . ES will review Tej's e-mail. . ES will post new version on 2008-01-16 or, at latest, 2008-01-17, and JH will call for e-mail vote to close 2008-01-21. - 2088: Covergroups in checkers [TT]. . TT has revised the proposal, DK agrees that his major issue is resolved. . JH will call for an e-mail vote to close 2008-01-21. - 2089: Final blocks in checkers [TT]. . TT will post one more revision today. Then JH will call for an e-mail vote to close 2008-01-21. . TT has uploaded the revision. Major items: - 1932: LTL Operators [DK, DB] . operator precedence . JM: a ##1 b throughout c[->1] will parse with LR(1). There will not be a shift reduce conflict in this case. . Discussion of whether LRM assumes LR(1) parsing. . JM will send mail to Brad Pierce about LRM parsing assumptions. . JM: If there are other parsing algorithms, we may need to consider the implications of operator precedence. . JH: We are running out of time. We may need to live with the revised precedence. . DB will update proposal, move precedence of next back where Johan had suggested it. . non-vacuity definition . Discussed JHs suggested. . JH: The prposal needs to have explicit non-vacuity for always, eventually. Also the current derived form for s_until does not give the right result. . DB will revise proposal and deposit on Wednesday. . DB uploaded. . JH will call for an email vote to run until 2008-01-28. - JH: People should suggest the next major item(s) based on our schedule. - LP will have 1698 ready for review this week. EC will review. General working items: - 2182: VPI for checkers [DK]. . JH will call for e-mail vote to close 2008-01-21. - 1901: Identifier for ## should be constant [EC] . YF, TT will review. - 2150: Disallow reference to automatic variables in action blocks and subroutine calls [MK] . MK updated the proposal. . JH will call for a vote to close 2008-01-21. - 1756: Assertion control tasks in initial blocks [EC] . DK does not want to drop this item. . DK: Did we say that we would use a different syntax? . JH: This would avoid the backward compatibility issue. . EC: Then the new syntax needs to be defined and it needs to be explained. - 1769: Elaboration-time assertions and error reporting [EC] . YF reviewed. . JH will call for an email vote to run until 2008-01-21. Other items ------------------------------------------------------------------------- Remaining Extension Schedule Legend: M: major item slot (2 concurrent) m: minor item slot (4 concurrnet) v: very minor item slot (no limit) d: draft preparation slot (no limit) Items in other Committees: -------------------------- 1503 // SV-CC [LP,BT are monitoring] 1599 // SV-CC [BT is monitoring] 1601 // SV-EC 1757 // SV-CC 1758 // SV-BC 1898 // SV-CC Late Items: ----------- v: 1687 // review due 2008-01-08 m: 1756 // due 2007-12-11 M: 1932 // due 2007-11-27 M: 1900 // due 2007-12-04 m: 1729 // due 2007-12-18 v: 1786 // due 2007-12-18; resolve in 1932 m: 2172 // draft due 2007-12-18 m: 2173 // draft due 2008-01-08 m: 2069 // draft due 2008-01-15 2008-01-15 M: 1667 ballot & revision M: 2005 review m: 2172 ballot & revision m: 2150 ballot & revision m: 1683 ballot & revision m: 1769 ballot & revision v: 1687 ballot & revision v: 1901 review d: 0966/1982 draft d: 2110 draft d: 2069 draft d: 1987 draft 2008-01-22 M: 2005 review M: 2110 review m: 2173 review m: 2150 ballot & revision m: 1769 ballot & revision m: 2069 review v: 1901 ballot & revision v: 1987 review d: 0966/1982 draft d: 2100 draft d: 1686 draft d: 1830 draft 2008-01-29 M: 2005 ballot & revision M: 2110 ballot & revision m: 2173 ballot & revision m: 0966/1982 review m: 2100 review m: 2069 review v: 1686 review v: 1830 review v: 1987 ballot & revision d: 1806 draft 2008-02-05 M: 2005 ballot & revision M: 2110 ballot & revision m: 2173 ballot & revision m: 0966/1982 ballot & revision m: 2100 ballot & revision m: 1806 review v: 1686 ballot & revision v: 1830 ballot & revision 2008-02-12 M: 2069 ballot & revision M: 1551 review m: 0966/1982 ballot & revision m: 2100 ballot & revision m: 2168 review m: 1806 review 2008-02-19 M: 2069 ballot & revision M: 1551 ballot & revision m: 2168 ballot & revision m: 1806 ballot & revision m: m: 2008-02-26 M: 1551 ballot & revision M: m: m: m: m: ================================================================ OLD Notes: ------ - Reminder of IEEE patent policy. Ballot results - 1682: Future value functions [DK] . Ballot failed. . DK will revise today and JH will call for a vote to close on 2007-12-24. - 1900: Checkers [DK] . Ballot failed. . The equivalence stated is not like other equivalences in simulation. DK will rework the language. JH says this is not equivalent for what we have been talking about requiring of the simulator. ES says maybe they should be said to be equivalent for formal tools. . DK will also clarify the second example with local variables. . DK will add an example to illustrate using matched. . DK will try to revise in two days. We will have 10-day ballot. - 1995: Assertions and checkers in for loops [ES] . Ballot passed, but with friendly amendments. . ES will modify and JH will call for a vote to close on 2007-12-24. - 2005: Glitches with immediate assertions [ES] . Ballot failed. . The proposal is already updated. JH will call for a vote to close on 2007-12-24. Old items: - 1503: VPI diagram of propertinst has no vpiArgument. . We will leave SV-CC to stabilize and pass this and then SV-AC can have a final look. - 1683: Relaxing rules for building multiclocked properties . JH will call for a vote to close on 2007-12-24. Major items: - 1932: LTL Operators [DK, DB] . JM: There is still the issue of the rewrite rules in the formal semantics document. JM: It is not necessary to state that the transformation T is applied to a clocked sequence. JM will write down comments on Clause 16. DB: Intent was to remove the part about leading clock and replace with 1. JM: It does not look as though this has been done. - 1667: Local variable arguments [JH] -- proposal not yet ready . EC, DB volunteered to review the proposal. General working items: - 1729: Immediate assume and cover [EC] . Proposal updated 2007-12-03. . MK will review. There were changes due to 1641. - 2088: Covergroups for checkers [TT] - 2089: Allow checker construct to include final blocks with immediate assertions [TT] . JH will look for the revised proposals in the next two days and call for 10-day vote along with the 1900 vote. - 1987: Verification statement as defined term [DB review] . JH will call for an e-mail vote on this to close on 2007-12-24. - 2091: Clarify where concurrent assertions may appear [TT review] . LP will post the proposal and then TT will review. - 2150: Disallow reference to automatic variables in action blocks and subroutine calls [MK] . Manisha will post in the next day or two. . YF will review. - 2172: Sequence if-else [JH] -- proposal not yet ready Other items Next Meeting: - 2008-01-08, two-hour slot. ------------------------------------------------------------------------- Extension Schedule Legend: M: major item slot (2 concurrent) m: minor item slot (4 concurrnet) v: very minor item slot (no limit) d: draft preparation slot (no limit) 2007-11-13 M: 1932 ballot & revision M: 1900 review m: 1757 ballot & revision m: 1898 review m: 1756 ballot & revision m: 1682 ballot & revision 2007-11-20 M: 1932 ballot & revision M: 1900 ballot & revision m: 1757 ballot & revision m: 1898 review m: 1756 ballot & revision m: 1682 ballot & revision d: 1503 draft d: 2033 draft 2007-11-27 M: 1932 ballot & revision M: 1900 ballot & revision m: 2005 review m: 1898 ballot & revision m: 1756 ballot & revision m: 1503 ballot & revision v: 2033 review d: 1667 draft d: 1683 draft 2007-12-04 M: 1900 ballot & revision M: 1995 ballot & revision m: 1898 ballot & revision m: 1756 ballot & revision m: 1503 ballot & revision v: 2033 ballot & revision d: 1667 draft d: 2150 draft d: 1683 draft 2007-12-11 M: 1667 review M: 1995 ballot & revision m: 1729 ballot & revision m: 1756 ballot & revision m: 1503 ballot & revision m: 2150 review m: 1683 review v: 1786 review d: 2172 draft 2007-12-18 M: 1667 review M: 1995 ballot & revision m: 1729 ballot & revision m: 2172 review m: 2150 review m: 1683 review v: 1786 ballot & revision d: 1627 draft 2008-01-08 JAN M: 1667 ballot & revision M: 2005 review m: 2172 ballot & revision m: 2150 ballot & revision m: 1683 ballot & revision m: 1769 review v: 1687 review d: 2173 draft d: 2069 draft d: 1901 draft 2008-01-15 M: 1667 ballot & revision M: 2005 review m: 2172 ballot & revision m: 2150 ballot & revision m: 1683 ballot & revision m: 1769 ballot & revision v: 1687 ballot & revision v: 1901 review d: 0966/1982 draft d: 2110 draft d: 2069 draft d: 1987 draft 2008-01-22 M: 2005 review M: 2110 review m: 2173 review m: 2150 ballot & revision m: 1769 ballot & revision m: 2069 review v: 1901 ballot & revision v: 1987 review d: 0966/1982 draft d: 2100 draft d: 1686 draft d: 1830 draft 2008-01-29 M: 2005 ballot & revision M: 2110 ballot & revision m: 2173 ballot & revision m: 0966/1982 review m: 2100 review m: 2069 review v: 1686 review v: 1830 review v: 1987 ballot & revision d: 1806 draft 2008-02-05 M: 2005 ballot & revision M: 2110 ballot & revision m: 2173 ballot & revision m: 0966/1982 ballot & revision m: 2100 ballot & revision m: 1806 review v: 1686 ballot & revision v: 1830 ballot & revision 2008-02-12 M: 2069 ballot & revision M: 1551 review m: 0966/1982 ballot & revision m: 2100 ballot & revision m: 2168 review m: 1806 review 2008-02-19 M: 2069 ballot & revision M: 1551 ballot & revision m: 2168 ballot & revision m: 1806 ballot & revision m: m: 2008-02-26 M: 1551 ballot & revision M: m: m: m: m:Received on Wed Jan 23 06:25:24 2008
This archive was generated by hypermail 2.1.8 : Wed Jan 23 2008 - 06:25:37 PST