[sv-ac] notes from SV-AC meeting 2008-01-08

From: John Havlicek <john.havlicek_at_.....>
Date: Tue Jan 08 2008 - 10:27:32 PST
Hi Folks:

My notes from today's meeting are attached.

Please let me know if corrections 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-34
Written by: John Havlicek

Date:  2008-01-08
Time:  16:00 UTC (10:00 CST) 

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


Agenda:
-------

- Reminder of IEEE patent policy.

Champions results
- Items to other committees

Ballot results
- 1682:  Future value functions [DK], passed 2007-12-24, friendly amendments
- 1683:  Relax multiclock rules [DK],  passed 2007-12-24
- 1987:  Add "verification statement to glossary", passed 2007-12-24 
- 1995:  Assertions and checkers in for loops [ES], passed 2007-12-24, comments
  from SB.
- 2005:  Glitches with immediate assertions [ES], failed 2007-12-24
- 2089:  Final blocks in checkers [TT], failed 2007-12-31
- 1900:  Checkers [DK], failed? 2008-01-07
- 2088:  Covergroups in checkers [TT], failed 2008-01-07

Old items:

Major items:
- 1932:  LTL Operators [DK, DB]
- 1667:  Local variable arguments [JH] -- proposal not yet ready

General working items:
- 2150:  Disallow reference to automatic variables in action blocks
  and subroutine calls [MK]
- 2091:  Clarify where concurrent assertions may appear [TT review]
- 1729:  Immediate assume and cover [late]
- 1756:  Assertion control tasks in initial blocks [EC]
- 1769:  Elaboration-time assertions and error reporting [EC]

Other items


Notes:
------

- Reminder of IEEE patent policy.

Champions results
- Items to other committees

Ballot results
- 1682:  Future value functions [DK], passed 2007-12-24, friendly amendments
  . DK:  The friendly amendments have been incorporated.
  . JH will ask the people who had friendly amendments to confirm that 
    they have been addressed.
- 1683:  Relax multiclock rules [DK],  passed 2007-12-24
- 1987:  Add "verification statement to glossary", passed 2007-12-24 
  . LP:  The friendly amendment was addressed.
- 1995:  Assertions and checkers in for loops [ES], passed 2007-12-24, comments
  from SB.
  . ES:  There are some minor rewording necessary.  
  . We should be able to voice vote the revised proposal in the next meeting.
- 2005:  Glitches with immediate assertions [ES], failed 2007-12-24
  . ES:  Have been working with Tej Singh and Doug Warmke.  Will check back
    with them and post a revised version by next week.  Possibly eliminate the
    event control feature if we can't converge.
- 2089:  Final blocks in checkers [TT], failed 2007-12-31
  . DK will work with TT as needed to converge on technical resolutions.
- 2088:  Covergroups in checkers [TT], failed 2008-01-07
  . DK will work with TT as needed to converge on technical resolutions.
- 1900:  Checkers [DK], failed? 2008-01-07
  . DK:  There were comments that needed to be addressed, so it doesn't 
    make sense to extend voting period for old version.
  . DK:  DB asked if checkers can be in loops.  Without 1995, no.  But a
    technical elaboration will be required.
  . JH will call for vote on 1900 on 2008-01-09 to run through 2008-01-15.

Old items:

Major items:
- 1932:  LTL Operators [DK, DB]
  . DB:  until will follow the same clock flow rules as "and" and "or".
  . JH:  Try using regular \tt font rather than bolding it.
  . Discussion about operator precedence.  Most people said they prefer
    a simpler interpretation so that, according to the LRM,

       a ##1 b throughout c[->1]

    is illegal and 

       a ##1 (b throughout c[->1])
    
    is legal.
  . JM will look back at the reasoning without the "don't care" interpretation 
    of non-parsing combinations.
  . JH will look back at JM's arguments and see if any other examples
    should be considered.
  . Discussion of lack of definition of |=^{non} for until, always, eventually.
  . TT:  best to leave undefined if we aren't certain.  Tools could report
    non-vacuous.
  . JH will try to think about |=^{non}.

Discussion of VPI
BT:  CC is busy and throughput is low.  AC needs to make first cut on VPI
  changes.
DK:  We will need help to create VPI material.  It would be good if BT could
  own 2182.

- 1667:  Local variable arguments [JH] -- proposal not yet ready
  . It's ready for vote, but there is no VPI update.  
  . JH will decide whether to call for vote on feature before adding the VPI.

General working items:
- 2150:  Disallow reference to automatic variables in action blocks
  and subroutine calls [MK]
  . Reviewed by YF, LP.
  . DK:  Are loop iterators allowed under some conditions?  1995 allows
    using assertions in loops and may use loop variable.  Does this 
    conflict with 2150?
  . MK:  Is it guaranteed that the loop variable will exist when the action
    block executes?
  . DK & MK will converge on the technical points and MK will revise the proposal.  
- 2091:  Clarify where concurrent assertions may appear [LP]
  . TT reviewed the outline.  TT still needs to review the proposal.
- 1729:  Immediate assume and cover [late]
  . MK looked at updated version and it looked fine.
  . JH will call for an e-mail vote.
- 1756:  Assertion control tasks in initial blocks [EC]
  . We need to converge on the technical disagreement.
- 1769:  Elaboration-time error reporting [EC]
  . YF will review.


-------------------------------------------------------------------------
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
  1648 // SV-EC
  1757 // SV-CC
  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
  m: 2172 // draft due 2007-12-18

2008-01-08 JAN
  M: 1667 ballot & revision
  M: 2005 review
  m: 2172 ballot & revision
  m: 2150 ballot & revision
  m: 1683 ballot & revision // resolved
  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:

================================================================
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 Tue Jan 8 10:53:43 2008

This archive was generated by hypermail 2.1.8 : Tue Jan 08 2008 - 10:56:02 PST