[sv-ac] revised notes for SV-AC meeting 2007-10-16

From: John Havlicek <john.havlicek_at_.....>
Date: Tue Oct 16 2007 - 12:02:23 PDT
Hi Folks:

I marked Bassam as attending.

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-24
Written by: John Havlicek

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


Agenda:
-------

- Reminder of IEEE patent policy.
- Review the list of Mantis items to opened based on our face-to-face.

Major items
- 1549:  Argument passing [DB, LP, JH]
- 1932:  LTL Operator [DK, DB]

General working items:
- 2005:  Glitches with immediate assertions [ES]
- 1995:  Assertions and checkers in for loops [ES]
- 1648:  Default disable [DK, EC]
- 1729:  Immediate assume, cover [EC]
- 1682:  Future value functions [DK]
- 1641:  Severity for general error messages [MK]
- 1757:  accept_on, reject_on [EC, DB]
- 1756:  Control of assertions in initial blocks [EC]
- 1900:  Checkers [ES]


Notes:
------

- Reminder of IEEE patent policy.

- Review the list of Mantis items to be opened based on our face-to-face.
  . VPI access to checker instances and sequences and properties in 
    procedural code.  AI:  TT
  . TT added Mantis 2088:  covergroups in checkers.
  . TT added Mantis 2089:  final blocks with immediate assertions added to checkers.
  . TT added Mantis 2093:  add output ports or an equivalent method of accessing the 
    results of a checker.
  . 1698 is the existing mantis item for sampled value functions outside of 
    assertions.
  . New mantis item for naming assertions.  How to turn off insertions in
    functions, e.g.?  Do we have assertion control for immediate assertions?
    ES:  The existing mechanism for immediate assertions may work.  DK:  unlikely
    to be able to solve this.  DK will open the mantis item.

- Status of D4 review.  What to do with minor mistakes that were in 
  the proposals?
  . Stu is implementing some policies for consitency that affect courier
    bold keywords in the text.
  . Committee thought we should try to take care of minor things without
    opening a new mantis item.
  . JH will work with the reviewers to create the response to the editor.
  . To make these official, we will voice vote the response to the editor.

- Voice vote on revision of 1757 to require explicit clocking events in
  sampled value functions referenced in the accept/reject conditions.
  8y/0n/1a(TT).  The chair was not eligible.

Major items:
- 1549:  Argument passing [DB, LP, JH]
  . We should add 0966, 1982 to our list for 2007-11-12.  Also MK will
    monitor 1350 to keep us informed of technical developments.
  . JH will call for email vote on 1549.  
- 1932:  LTL Operator [DK, DB]
  . Non-vacuity definition has some problems.  
  . There is a definition from the literature that would give non-vacuity
    for the various subproperties.  It may be expensive to support and 
    gives a lot of coverage goals.
  . Discussed implication, always, until.  There are issues with 
    using the derived rules for non-vacuity.
    * What is intuitively desirable for until seems to require integrating
      elements of the satisfaction definition.  May need to keep track
      of negation parity.
  . Discussed decoupling 1932 from non-vacuity.  Better to undefine non-vacuity 
    for properties involving until, etc. than to define it liberally.
  . JM:  Will it be helpful to make list of examples and the desired result
    for non-vacuity?  JH thinks yes.
  . Reviewers JM and JH will put forth extra effort to get feedback to DB.
  . JH will send 1932 comments to DB directly.


General working items:
- 2005:  Glitches with immediate assertions [ES]
  . There was agreement on how to proceed in the face-to-face.
  . There has been resistence to this approach and extended discussion 
    in SV-BC.
  . Discussed syntactic well-definedness of the top of a procedural block.
  . ES will create a working document to capture the issues and examples.
- 1995:  Assertions and checkers in for loops [ES]
  . New version was posted before the face-to-face.  
    There is a version dated 2007-09-27.  TT & DB will review.
  . LP:  Changes on inferred enabling condition in 1737 overlap with these
    changes.
  . ES will review 1995 with respect to 1737.
- 1648:  Default disable [DK, EC]
  . JH will dig up the deadline date from WG.
  . Nothing to be done until the deadline expires (except to put this
    on the list).
- 1729:  Immediate assume, cover [EC]
  . Need to align with 1641 and Draft4.
  . MK will send mail about what needs to be aligned.
- 1641:  Severity for general error messages [MK]
  . MK:  This item is ready for vote.
  . JH will call for e-mail vote.
- 1756:  Control of assertions in initial blocks [EC]
  . EC:  This item is ready for vote.
  . JH will call for e-mail vote

DK: 1731 was approved and feedback came back from Champions (JH).  JH
will review the revised proposal and determine what if any further
changes are needed.  JH will then either give feedback to DK or call
for vote.

We did not get to these items:

- 1682:  Future value functions [DK]
- 1900:  Checkers [ES]

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

2007-10-23 at 16:00 UTC (11:00 CDT), 2 hour slot.
Received on Tue Oct 16 12:02:58 2007

This archive was generated by hypermail 2.1.8 : Tue Oct 16 2007 - 12:03:09 PDT