Minutes of IEEE P1800 SV-AC meeting #2007-46 Written by: Dmitry Korchemny Date: 2008-03-18 Time: 16:00 UTC (9:00 PST) Dial-in information: -------------------- Toll number: +1 916-356-2663 Toll free number (US): 888-875-9370 (U.S. toll-free) Bridge: 4, Passcode: 2101948 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: v[xxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) v[xxxxxxxxxxxxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) n[-------------------------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) v[xxxxxxxx-xxxxxxxxx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) v[xxxxxxxxxxxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale) t[x-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel – Provisional Chair) v[-xx-x-xxxxxxxxx-xxxxxxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics) n[-------x-x-------------------------------------------------] Ah-Lam Lee (Qualcomm) n[----------------------------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics) n[-------------------x------------x--xxx.....................] Joseph Lu (Altera) n[-----x-x--xxxxxxxxxxxxxxxxxxx..............................] Johan Martensson (Jasper) n[-------------------------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) v[xxxxxxxxxxxxxxx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) v[xxxxx-xxxxxxxxxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) n[-----------------x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) v[x-x-x-xxx-xxxxxx-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) v[xxxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems – Provisional Co-Chair) |------------------------------------------------------ attendance on 2008-03-18 |-------------------------------------------------------- voting eligibility on 2008-03-18 Agenda: ------- - Reminder of IEEE patent policy. See: http://standards.ieee.org/board/pat/pat-slideset.ppt Champions’ results: 2173 Add case construct for properties Passed Create a new Mantis item for vacuity and default issues Create a new Mantis item for the VPI stuff? 2100 Add synchronous resets Passed Address Shalom’s friendly amendments (done) 2069 Formal semantics for coverage is missing Address John’s and Lisa’s comments 2005 Solution for glitch problem in immediate assertions Passed Address friendly amendments 1932 Introduce LTL and other temporal operators Resolve keyword issue 1852 Ballot Feedback Issue STU2: Declarations on Assertions 1849 Update VPI object diagrams for immediate assume, cover 1833 JEITA: 16.3 Precise definition of immediate assertion 1786 Definition of "if else" in Annex F seems broken 1982 16.7: Description of actual arguments is unclear and maybe also inconsistent with other description of $ Passed (as duplicate) Other: - LP: Can the number of ticks in $past be variable? - LP: vpiAssertionReset and vpiAssertionKill for immediate assertions - SB: 16.3 “shall” à “will” (two occurrences) - SB: 1641: explicitly delete the phrase ", which can be suppressed in a tool-specific manner" in 16.3. - DM: Ambiguity in concurrent assertions: string is not allowed, string.len is (?), etc. Notes: ------ - Reminder of IEEE patent policy. - Champions’ results: 2173 Add case construct for properties . YF will split the proposal into three: basic proposal (approved by the champions), vacuity-related proposal and the VPI related proposal. . The voce vote scheduled for 2008-03-20 2100 Add synchronous resets . YF will fix typos reported by SB . The voce vote scheduled for 2008-03-20 2069 Formal semantics for coverage is missing . DK sent the updated version addressing JH and LP comments. . DK will call to vote. 2005 Solution for glitch problem in immediate assertions . We hold a voice vote on the changes made by ES. . The updated proposal passed: 7y/0n/0a 1932 Introduce LTL and other temporal operators . Discussion about keywords introduced by this proposal . JH: introducing strong and weak operator for arbitrary properties is not feasible in the current time frame. . DK: using strong as a keyword instead of s_ will make the temporal formulas unreadable. . DK: there is no viable alternative for “until”. . JH: “nexttime” is an accepted pronunciation of the operator NEXT. . EC: “next_time” vs. “nexttime”. . JH: “nexttime” is an accepted name. . DK: Prefix “s_” vs. suffix “_s”. In some cases “s_” is more readable, and sometimes “_s” is. . JH: “s_” reflects the English syntax, while “_s” makes the main part of the word more readable. . JH: Let’s keep the current syntax. . Voice vote on keeping the current syntax with the only change “(s_)next” -> “(s_)nexttime” Passed: 7y/0n/0a . DB sent the updated version of the proposal. The voice vote on the updated proposal will take place on 2008-3-20. 1852 Ballot Feedback Issue STU2: Declarations on Assertions 1849 Update VPI object diagrams for immediate assume, cover 1833 JEITA: 16.3 Precise definition of immediate assertion 1786 Definition of "if else" in Annex F seems broken 1982 16.7: Description of actual arguments is unclear and maybe also inconsistent with other description of $ Passed (as duplicate) DK will ask NK to conditionally put the proposals under vote to the champions’ agenda for 2008-3-20. Other: - LP: Can the number of ticks in $past be variable? . DK expressed concern about letting number of ticks to be a variable: PSL has a limitation that the number of ticks should be constant. Otherwise there may be decidability problems. . JH: If the type domain is bounded, the MC will remain decidable. . LP will open a new Mantis item clarifying that the number of ticks should be a constant - LP: vpiAssertionReset and vpiAssertionKill for immediate assertions . No action - SB: 16.3 “shall” à “will” (two occurrences) . DK will open a new Mantis item. . DK will ask NK about the next steps. - SB: 1641: explicitly delete the phrase ", which can be suppressed in a tool-specific manner" in 16.3. . Already done in 1641. - DM: Ambiguity in concurrent assertions: string is not allowed, string.len is (?), etc. . JH will open a new Mantis item. Opens. .JH: Needs to mention restrict among the assertion statements. .EC will send JH the Word document of 1806 and JH will make relevant changes there. . The voce vote scheduled for 2008-03-20 The next SV-AC meeting will occur on Thursday, 2008-03-20 at 14:00 UTC (7:00 AM PST).