[sv-ac] notes from SV-AC meeting 2007-10-30

From: John Havlicek <john.havlicek_at_.....>
Date: Tue Oct 30 2007 - 12:01:58 PDT
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-26
Written by: John Havlicek

Date:  2007-10-30
Time:  16:00 UTC (11:00 CDT) 

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[xxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel)
vv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)     
nn[-------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys)
vv[xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale)
tt[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair)
vv[xxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair)
vv[xxxxxx-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[xxxxxxxxxx..............................] Johan Martensson (Jasper)
nn[------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale)
vv[x-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
vv[x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel)
nn[x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics)
vv[xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys)
vv[-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems)
   |---------------------------------------- attendance on 2007-10-30
 |------------------------------------------ voting eligibility on 2007-10-30
|------------------------------------------- new voting eligibility


Agenda:
-------

- Reminder of IEEE patent policy.

- Discussion of name resolution questions involving "bind".  
  Gord Vreugdenhil will join.

- D4 Review
  . JH will work with the D4 reviewers to create the response to the editor.
    To make these official, we will voice vote the response to the editor.

- Extension period plan (due 2007-11-12)
  . 2007-10-30 due date for items and effort plans.

- Voice vote on friendly amendments
  . 1549 (missing word "results" in "results in illegal syntax").

Ballots closing 2007-10-30:
- 1567:  In Syntax 22-7 there should be no semicolon [JH].
- 1682:  Future value functions [DK].  Negative vote.

Ballots closing 2007-11-05:
- 1648:  Default disable [DK, EC].
- 1731:  Sampled value functions with arbitrary clocks [DK].
- 1757:  accept_on, reject_on [EC, DB].
- 1737:  Incomplete fix from 1381

Feedback State:
- 1641:  Severity for general error messages [MK]
  . Friendly amendments and feedback from Shalom addressed?  
  . E-mail ballot or voice vote?
- 1601:  New keyword for untyped formal arguments [LP]
  . 1549 has passed, so this needs to be revised and aligned.
- 1729:  Immediate assume, cover [EC]
  . AI:  MK will send mail about what of 1729 needs to be aligned with 1641.

Major items:
- 1932:  LTL Operator [DK, DB]
- 1900:  Checkers [DK]

General working items:
- 1756:  Control of assertions in initial blocks [EC]
  . DK:  Let's try to write sketches of two possible solutions.
    One can be adding an argument to the assertion control, another
    to add another control task.  DK will write an e-mail with the
    sketches.  Then we will get feedback.
- 2005:  Glitches with immediate assertions [ES]
- 1995:  Assertions and checkers in for loops [ES]
- Other items


Notes:
-------

- Reminder of IEEE patent policy.

- D4 Review
  . JH will work with the D4 reviewers to create the response to the editor.
    To make these official, we will voice vote the response to the editor.
  JH will finish a.sap and send for review.  We will voice vote in the 
  next meeting.

- Extension period plan (due 2007-11-12)
  . 2007-10-30 due date for items and effort plans.  JH has collected
    the effort estimates so far, but he did not make his own.
  . People will review the mantis items to see what else we may
    want to work on in the extension period.  We will take one
    more week to get effort estimates for such items.
  . DK will keep the growing list of items to be worked on in
    the extension and send it out periodically so that people can
    confirm that their items are on the list.

- Voice vote on friendly amendments
  . 1549 (missing word "results" in "results in illegal syntax").
  . Voice vote to approve:  9y/0n/0a.

- 1728:  Let [DK].
  . Have the friendly amendments been addressed?  Has the proposal been 
    aligned to D4?  Do we need to have another e-mail ballot?
  . Voice vote to approve:  8y/0n/1a [Erik Seligman abstained].

Ballots closing 2007-10-30:
- 1567:  In Syntax 22-7 there should be no semicolon [JH].
- 1682:  Future value functions [DK].  Negative votes.
  . Feedback from DB has already been addressed.
  . Discussion of feedback from MK.  DB argued that we don't have
    a definition of when attempts end, regardless of the future value
    functions.  We talked about not saying anything about when these
    attempts end or when the action blocks execute.  MK will send a
    suggestion about rewording.

- Discussion of name resolution questions involving "bind".  
  Gord Vreugdenhil will join.
  . GV:  Context of bind statement and context of target are important.
  . GV:  Names in the bind statement are to be resolved in the context
    of the bind target.  Exactly what are the assumptions about this
    statement?  References to types are problematic.  
  . GV:  A bind should not impact name resolution decisions that have
    already been made in the target.
  . GV:  Names that can be referenced in bind must be valid hierarchical
    references in target.  
  . GV:  How do we deal with a type reference in bind?  Type and package 
    references in a bind statement resolve in the context of the bind
    statement.
  . JH:  We need to be able to get a bound instance to pick up a type
    parameter override from a target instance.  How do we specify that?
  . GV:  If you want to use something as a type from the target, you would 
    need to use type(yadda).

Ballots closing 2007-11-05:
- 1648:  Default disable [DK, EC].
- 1731:  Sampled value functions with arbitrary clocks [DK].
- 1757:  accept_on, reject_on [EC, DB].
- 1737:  Incomplete fix from 1381

Feedback State:
- 1641:  Severity for general error messages [MK]
  . Friendly amendments and feedback from Shalom addressed?  
  . E-mail ballot or voice vote?
  . Manisha has revised according to Shalom's comments.
  . Voice vote to approve:  7y/0n/2a [Johan Martensson, Erik Seligman abstained].
- 1601:  New keyword for untyped formal arguments [LP]
  . 1549 has passed, so this needs to be revised and aligned.
  . JH will call for an e-mail vote.
- 1729:  Immediate assume, cover [EC]
  . AI:  MK will send mail about what of 1729 needs to be aligned with 1641;
    then EC will revise; then JH will call for e-mail vote.

Major items:
- 1932:  LTL Operator [DK, DB]
  . DB:  There has been progress on the vacuity definition.  JM's definition
    may be better than the existing one, but it does not seem to solve the 
    problem with the until operator.

  . DB:  Question about clocking for eventually, e.g.
 
       @(clk1) a |-> eventually @(clk2) b

    JH:  In this case eventually should be clocked at clk1.

  . X[0] as alignment to inherited clock.  DB mentioned Dana Fisman's 
    presentation that involved this topic.  
  . Issues about multiclocks and LTL operators.  1683 is not being pushed
    yet.  DB will need to include restrictions on clock changes with LTL
    operators for now.
  . JM:  We should not delay 1932 based on coverage ideas.
  . DB will say that vacuity for LTL until is not defined.

- 1900:  Checkers [DK]
  . DK did not receive feedback on the checkers proposal.
  . Missing formal semantics for free variables.  No feedback
    on the rest.
  . We don't have convergence on the non-deterministic free variables.
  . DK:  Universal quantification is important, but not the only usage.
    Additional syntax should be used for different usages.

General working items:
- 1756:  Control of assertions in initial blocks [EC]
  . DK:  Let's try to write sketches of two possible solutions.
    One can be adding an argument to the assertion control, another
    to add another control task.  DK will write an e-mail with the
    sketches.  Then we will get feedback.
  . DK:  Most people preferred the first option.  MK has not sent 
    feedback yet.
  . EC:  How will you run these in formal?


We did not get to these items:

- 2005:  Glitches with immediate assertions [ES]
- 1995:  Assertions and checkers in for loops [ES]


Next meeting: 
-------------

2007-11-06 at 17:00 UTC (10:00 CST), 2 hour slot.
Received on Tue Oct 30 12:02:28 2007

This archive was generated by hypermail 2.1.8 : Tue Oct 30 2007 - 12:02:41 PDT