[sv-ac] notes from SV-AC meeting 2008-02-12

From: John Havlicek <john.havlicek_at_.....>
Date: Wed Feb 13 2008 - 03:49:01 PST
Hi Folks:

My notes from our meeting 2008-02-12 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-39
Written by: John Havlicek

Date:  2008-02-12
Time:  16:00 UTC (10:00 CST) 

Dialin information:
-------------------

Toll number:   +1 647 723 3904

Country                 Toll Free 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[-xxxxxxxxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel)
vv[xxxxxxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)     
nn[--------------------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys)
vv[xx-xxxxxxxxx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale)
tt[xxxxxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair)
vv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair)
vv[xxxxxxxxx-xxxxxxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics)
nn[-x-x-------------------------------------------------] Ah-Lam Lee (Qualcomm)
nn[----------------------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics)
nn[-------------x------------x--xxx.....................] Joseph Lu (Altera)
nn[-x--xxxxxxxxxxxxxxxxxxx..............................] Johan Martensson (Jasper)
nn[-------------------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale)
vv[xxxxxxxxx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
vv[xxxxxxxxxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel)
nn[-----------x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics)
vv[xxx-xxxxxx-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys)
vv[xxxxxxxxxxxxx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems)
   |---------------------------------------------------- attendance on 2008-02-12
 |------------------------------------------------------ voting eligibility on 2008-02-12
|------------------------------------------------------- new voting eligibility


Agenda:
-------

- Reminder of IEEE patent policy.

Champions e-mail ballot 2008-02-04
- Approved
  . 1549 Argument types
- Insufficient participation
  . 1667 Local variable arguments
  . 1668 Local variable initializers
  . 1729 Immediate assume and cover
- Failed with negative vote
  . 1728 Let
  . 1900 Checkers
  . 1995 Assertions and checkers in for loops

Ballot results
. 1987 Assertion statement
. 2069 Formal semantics for coverage
. 2088 Allow covergroups in checkers
. 2110 Add checkers in procedural for loops
. 2168 Formal semantics for edge-sensitive clocks
. 2182 VPI diagrams for checkers
. 2250 VPI changes for LTL operators

Procedural topics
- DK to tally ballots from now on?
- We are entering the period of the massive review of SV-AC proposals
  by the champions, and this requires quick voting for the changes
  addressing the friendly amendments. The current meeting scheme
  allows approving a given proposal once in two or three weeks:
  addressing friendly amendments from the champions takes one week,
  voting takes another week and addressing friendly amendments from
  SV-AC takes yet another week.  Therefore I suggest changing the
  schedule of our meetings to have three meetings a week: one one-hour
  meeting for discussions and voice voting and two 15-minute meetings
  for voice voting only.

Old items
. 1932 LTL operators
  - voice vote minor changes, ask to have added to Champions agenda
. 1900 Checkers [on Champions agenda]
  - require another e-mail ballot
. 1728 Let [on Champions agenda]
  - voice vote minor changes
. 1995 in feedback [on Champions agenda]
  - voice vote minor changes
. 2150 Disallow automatic variables in subroutine calls and action blocks
  - voice vote friendly amendments, ask have added to Champions agenda
. 1503 Assertion VPI changes
  - Is SV-CC still working on this?

E-mail ballots to be called:
. 1698 Semantics of sampled value functions outside assertions
. 2100 Synchronous resets
. 1901 Identifier for ## should be constant

2100 needs review or ballot
2173 needs review or ballot

Items with actions in other committees
. 1599 API and VPI changes for 0805
  - to be re-approved by SV-CC
. 1769 Elaboration-time assertions
  - to be reviewed and approved by SV-BC
. 2005 Glitches with immediate assertions
  - to be reviewed and approved by SV-CC
. 2088 Covergroups in checkers
  - to be reviewed and approved by SV-EC
. 2089 Covergroups in checkers
  - to be reviewed and approved by SV-BC and SV-EC

Other items


Notes:
------

- Reminder of IEEE patent policy.

Champions e-mail ballot 2008-02-04
- Approved
  . 1549 Argument types
- Insufficient participation
  . 1667 Local variable arguments
  . 1668 Local variable initializers
  . 1729 Immediate assume and cover
- Failed with negative vote
  . 1728 Let
  . 1900 Checkers
  . 1995 Assertions and checkers in for loops

Ballot results
. 1987 Assertion statement
  - Passed no friendly amendments.  JH to move to resolved.
. 2069 Formal semantics for coverage
  - Failed due to insufficient votes.
  - SV-AC approved extending this ballot for one more day.
    8y/0n/0a.  JH to send email to that effect.
. 2088 Allow covergroups in checkers
  - Passed with friendly amendments.
  - Voice vote to approve friendly amendments.
    8y/0n/0a.  Approved.  JH to move to resolved.
. 2110 Add checkers in procedural for loops
  - Passed with friendly amendments.
    8y/0n/0a.  Approved.  JH to move to resolved.
. 2168 Formal semantics for edge-sensitive clocks
  - Passed, no friendly amendments.  JH to move to resolved.
. 2182 VPI diagrams for checkers
  - Passed, friendly amendments.
    8y/0n/0a.  Approved.  JH to send message:
    SV-AC request SV-CC to review and approve 2182.
. 2250 VPI changes for LTL operators
  - Passed, friendly amendments.
    8y/0n/0a.  Approved.
    SV-AC request SV-CC to review and approved 2250.
    Message approved.  JH will send it.

Procedural topics
- DK to tally ballots from now on?
- We are entering the period of the massive review of SV-AC proposals
  by the champions, and this requires quick voting for the changes
  addressing the friendly amendments. The current meeting scheme
  allows approving a given proposal once in two or three weeks:
  addressing friendly amendments from the champions takes one week,
  voting takes another week and addressing friendly amendments from
  SV-AC takes yet another week.  Therefore I suggest changing the
  schedule of our meetings to have three meetings a week: one one-hour
  meeting for discussions and voice voting and two 15-minute meetings
  for voice voting only.

  . Add meetings at 07:00 PST on 2008-02-21 and 2008-02-28.  Further 
    meetings in an extension if granted.

  . SV-AC request that the P1800 WG grant an extension until 2008-03-31 
    for the purpose of addressing feedback from Champions and to 
    work with SV-CC on VPI/API changes for proposals that are resolved
    in SV-AC by the 2008-02-28 deadline.

    voice 7y/0n/0a
    JH will send this to the working group.

Old items
. 1932 LTL operators
  - voice vote minor changes, ask to have added to Champions agenda
    8y/0n/0a.  Approved.  DB needs to implement the last change and send
    email.  Then JH will move to resolved.
. 1900 Checkers [on Champions agenda]
  - require another e-mail ballot
    DK made numerous changes from Champions.
    DK will update to address one outstanding comment from JH.  JH will call
    for an email vote.
. 1728 Let [on Champions agenda]
  - voice vote minor changes
    8y/0n/0a.  Approve fixing parenthesis mismatch.  JH will move to resolved.
. 1995 in feedback [on Champions agenda]
  - voice vote minor changes
    8y/0n/0a.  Approved.  JH will move to the resolved state.
. 2150 Disallow automatic variables in subroutine calls and action blocks
  - voice vote friendly amendments, ask have added to Champions agenda
    JH will look for mail from Manisha that this is implemented and then 
    move state to resolved.
. 1503 Assertion VPI changes
  - Is SV-CC still working on this?
    BT says it is still being resolved in SV-CC.

Champions Major Negative Feedback on 1995:         

This proposal is essentially creating a generate block within a
procedural context. I'm fine with limiting this to assertion
statements for now, but that does alleviate addressing all the issues
surrounding generated code. For example each assertion statement is
replicated in the loop (including nested loops) and a generate block
label needs to be created for every instance of each. The loop
iterator should be treated as a genvar constant within each instance
of the assertion statement.

SV-AC Response:

This is incorrect.  The assertion is not being rewritten, and therefore
no artificial generate block is created.  The only effect is that the
assertion is executed several times during the same time slot.  Erik
sent the following clarification:

   ... this proposal was specifically written (with help from your
   co-worker Gord) to *not* treat these as generate loops, and thus avoid
   the (very valid) issue you mention.  Can you please re-review, in
   consultation with Gord?  Thanks!

Champions should review this.

Voice vote to approve this response:  8y/0n/0a.

Champions Major Negative Feedback on 1728:

It seems very odd that the let statement is allowed on an immediate
assertion, which is no more complex than a 'if' statement, but not
allowed in any Boolean expression. I understand the SV-AC rush to add
features to the language and limiting those features to assertions,
but limited this kind of feature to assertions does not serve the end
user and the language very well. If there are issues preventing wider
adoption of this feature, let then be flushed out now.

SV-AC Response:

The original intent of SV-AC was to make this construct general, but
since other committees did not have sufficient time budget for
reviewing it, it was decided to limit it for assertions only.  The
proposal is formulated in the way that it can be extended in the
future for additional areas of usage, and it is safer to publish first
a limited version of the proposal than to come with an insufficiently
elaborated general proposal.  We believe that this feature is
essential for building assertion libraries and for doing formal
verification.  SV-AC is already responsible for elaboration of
templates for concurrent assertions (sequence and property
constructs), and we see it as reasonable for SV-AC to provide a
template for immediate assertions (let construct).

Voice vote to approve this response:  8y/0n/0a.

Champions Major Negative Feedback on 1900

This proposal needs to be addressed when it can have the full
attention of all the committees as effects every part of the language.
Otherwise, I feel that this enhancement goes beyond the level of
enhancements authorized by the P1800 PAR in embedding a new language
with SV. The number of keywords and statements being introduced can
not be thoroughly reviewed with the resources we have for the current
par.

SV-AC Response:

This proposal was a focal point of SV-AC this year. It generalizes the
notion of a concurrent assertion and is a gating capability for
building assertion libraries and for doing formal verification in
SystemVerilog.  We believe that the main application of checkers
belongs to the SV-AC area, though this construct is also useful for
coverage collection, and therefore it is within the bounds of the
P1800 PAR.  The number of introduced keywords is relatively small:

-          checker/endchecker

-          [free] checkvar

-          initial_check/always_check

If the time required for reviewing this proposal is not sufficient, we
believe that this issue should be addressed by the WG to extend the time
line in order to allow proper reviewing of this proposal and addressing
the reviewers' comments.

Voice vote 8y/0n/0a.   Response is approved.


E-mail ballots to be called:
. 1698 Semantics of sampled value functions outside assertions
  - LSB should be least significant byte.
. 2100 Synchronous resets
. 1901 Identifier for ## should be constant
. 2173 Property case

Items with actions in other committees
. 1599 API and VPI changes for 0805
  - to be re-approved by SV-CC
. 1769 Elaboration-time assertions
  - to be reviewed and approved by SV-BC
. 2005 Glitches with immediate assertions
  - to be reviewed and approved by SV-CC
. 2088 Covergroups in checkers
  - to be reviewed and approved by SV-EC
. 2089 Covergroups in checkers
  - to be reviewed and approved by SV-BC and SV-EC

Other items

-------------------------------------------------------------------------
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 returned from Committees:
-------------------------------
  1601 // SV-EC
  1599 // SV-CC, revision required
  1758 // SV-BC, revision required

Items in other Committees:
--------------------------
  1503 // SV-CC [LP,BT are monitoring]
  1757 // SV-CC
  1898 // SV-CC

Late Items
  m: 1756 // due 2007-12-11; review
  M: 1932 // due 2007-11-27; ballot & revision
  v: 1786 // due 2007-12-18; resolve in 1932
  v: 1687 // due 2008-01-15; open
  m: 2172 // due 2008-01-15; open
  d: 2173 // draft due 2008-01-08
  m: 2150 // due 2008-01-22; ballot & revision
  d: 0966/1982 // draft due 2008-01-22; open
  v: 1901 // review due 2008-01-15
  m: 2100 // review due 2008-01-29
  v: 1686 // review due 2008-01-29
  v: 1830 // review due 2008-01-29
  d: 1806 // draft due 2008-01-29

Schedule:
---------
2008-02-05
  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 Wed Feb 13 03:51:20 2008

This archive was generated by hypermail 2.1.8 : Wed Feb 13 2008 - 03:51:29 PST