Minutes of IEEE P1800 SV-AC meeting #2007-46

Written by: Dmitry Korchemny

Date:  2008-03-18

Time:  16:00 UTC (9:00 PST)

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-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).

 Create your own business wiki!HelpPublic, not yet premium Privacy Policy RSS