[sv-ac] Minutes from SV-AC meeting 10/26/2010

Minutes from SV-AC Meeting
Date: 2010-10-26
Time: 16:00 UTC (9:00 PDT)
Duration: 1.5 hours

Dial-in information:
--------------------
Meeting ID: 38198

Phone Number(s):
1-888-813-5316 Toll Free within North America

Live meeting: https://webjoin.intel.com/?passcode=4396846

Agenda:
-------
- Reminder of IEEE patent policy.
See: http://standards.ieee.org/board/pat/pat-slideset.ppt

- Minutes approval

- New Guidelines for Mantis Proposals
     1. Mantis proposal must be in PDF format.
     2. Mantis proposal must have a title showing the Mantis number

- Champions Feedback:
Friendly Amendments:
1. 2485: Proposal uploaded. Voice vote.

Failed:
1. 2205: SV-AC $asseroff, $assertkill and $asserton description is
ambiguous
2. 2412: SV-AC Allow clock inference in sequences
3. 2938: SV-AC Surprising (to some users) interaction between deferred
assertions & short-circuiting

- Issue Resolution:
2328 - Review and relax restrictions on data types in assertions
2904 - Clarify when disable iff condition must occur relative to
starting and ending of an attempt
3135 - Verbal explanation of nexttime and always is misleading for
multiple clocks

- Enhancement progress update
2578 - Vacuity

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

Attendance re-initialized on 2010-07-06:

   v[xxxx-x-xxxxx--xxx] Laurence Bisht (Intel)
   v[xx-xxxxxxxxxxxxx-] Eduard Cerny (Synopsys)
   v[xxxx-xxxxx-xxxxxx] Ben Cohen
   n[-x-xxx-x--xxxxxxx] Surrendra Dudani (Synopsys)
   n[x---xxxx---x-xxxx] Dana Fisman (Synopsys)
   v[x-xxxx-x-xxxxxxxx] John Havlicek (Freescale)
   v[-xxx-xxxxxxxxxxxx] Tapan Kapoor (Cadence)
   t[--xxxxxxxxxxxxxxx] Dmitry Korchemny (Intel ¿ Chair)
   v[--xxxxxx-xxxxxxxx] Scott Little (Freescale)
   v[xxxxxxxxx-xxxxxxx] Manisha Kulshrestha (Mentor Graphics)
   v[xxxxxxxxxxxxxxxxx] Anupam Prabhakar (Mentor Graphics)
   v[x-xx--xxxxxxx-xxx] Erik Seligman (Intel)
   v[--xxxxxx-xxxxxxx.] Samik Sengupta (Synopsys)
   v[xxxxxxxxxxxxx-xxx] Tom Thatcher (Oracle ¿ Co-Chair)
     |- attendance on 2010-10-26
   |--- voting eligibility on 2010-10-26

Minutes:
--------
- Reminder of IEEE patent policy.
See: http://standards.ieee.org/board/pat/pat-slideset.ppt

- Minutes approval
Ben: Move to approve minutes
Erik: Second
        Vote results 6y, 0n, 0a

- New Guidelines for Mantis Proposals
     1. Mantis proposal must be in PDF format.
     2. Mantis proposal must have a title showing the Mantis number

- Champions Feedback:

Proposals with Friendly Amendments:
1. 2485: Proposal uploaded. Voice vote.
Tom: Proposal changed "can" to "may" in final sentence to address
        Champions feedback.
Erik: Move to approve
John: Second
        Vote results; 6y, 0n, 0a

Proposals that Failed the Champions Vote:
1. 2205: SV-AC $asseroff, $assertkill and $asserton description is
ambiguous
Erik: Removed changes to section 20.13 (This section will be deleted by
        another Mantis item).
Ed: Move to approve
John: Second

(Laurence joined)

        Vote results: 7y, 0n, 0a

2. 2412: SV-AC Allow clock inference in sequences
Champions feedback: clock inference rules repeated in two places.
Anupam: Changed to remove duplicate set of rules.
        Changed "note that:" to a real NOTE"
        Changed "should" to "shall" in a couple places
John: Understanding is that notes are not normative
        If these are rules that are required, they should not be notes.
        Don't use the word "note" in the text unless it is a note.
        If it is a note, it is not normative.
Anupam: Should last sentence on P3 be a note?
John: Does it follow from other text?
John: Looks like it should not be a note.
Manisha: Same rule is mentioned in 16.6
John: But doesn't follow for sampled value functions. This sentence should
        not be a clock. Also, the sentence should use the work "shall" instead
of "must"
Ed: Should put in a reference to 16.6
Anupam: Should rule be moved to 16.6?
Manisha & Ed: The rule would seem to be out of place in 16.6

Anupam Will work more on the proposal.

JOhn: Another Mantis item dealt with clarifying disable may affect this
        proposal

John: If we move the rule to 16.9, should we also remove the example?
Manisha: The example is not really important. We should remove it.

Anupam: Will update the Mantis sometime this week.

3. 2938: SV-AC Surprising (to some users) interaction between deferred
assertions & short-circuiting

Erik: Fixed syntax errors. Changed last sentence to be more neutral
        sounding.
John: Extra space before comma in last sentence

Erik: Move to approve with friendly amendment to remove space before comma
John: second.
        Vote results: 7y, 0n, 0a

- Issue Resolution:
2328 - Review and relax restrictions on data types in assertions
John: No progress

2904 - Clarify when disable iff condition must occur relative to
starting and
        ending of an attempt
Tom: Ready for an e-mail ballot?
John: I think so.
Tom Will call an e-mail ballot for 2904

3135 - Verbal explanation of nexttime and always is misleading for
multiple clocks
Dana: Had been voted upon earlier. Implemented most friendly amendments.
        Erik had suggested incorporating added paragraph into the original
        descriptions of the operator function.

Erik: Other amendments:
        n+1's should be n+1'th

Ed: Why mix tick and cycle? Make language consistent throughout.
Erik: Had suggested that added paragraph be included in the original
        descriptions of operator function, but is okay with current proposal
Ed: Clock tick is a time step where clocking event occurs, while cycle
        is a time period.

Tom: Will call for an e-mail ballot when proposal is updated.

- Enhancement progress update
-2578 - Vacuity
Ben: Has written a new proposal. It's a straw-man proposal to start
        discussion.
Dana: Why do we need syntactic definition?
        Lots of opinions about Vacuity definitions. Would precisely
        defining vacuity force one definition on the whole community, when
        we are not even sure what the definition should be?
Ed: Different requirements for model checking, simulations.
        Simulation might not be able to determine vacuity.
Dana: Can you even define an "attempt" precisely.
Ed: Can define where an attempt begins, but when the attempt ends is
        not defined precisely.
John: We have a finite trace semantics, so it is possible to define.
John: Agree with most comments, Dana.
        We went down this path because certain types of reporting were
        required by LRM. This forced us into a definition, which may
        be a flawed definition.
Dana: If you have syntactic definition: then semantically equivalent
        formulas would have different vacuity.
John: Dana's comment: we are not ready to define vacuity precisely.
Ben: So ambiguity is better?
Ed: For simulation case: would it be OK to limit to the top-level
        property? Any vacuity which is too complicated would kill performance.
Dana: Several different papers define vacuity differently
        There is no single definition that the community agrees with.
Ben: But would like some definition.
Ed: Maybe we define some rules. Users will not be happy if different
        simulators give different results.
Dana: Will look around to collect different definitions
Ben: Hopefully, the definitions won't be too mathematical?
John: Well, the mathematics behind the definition must exist.
John: We had to make a complete definition before we were ready. We know
        there are problems with the current definition.
Ed: Maybe we just define vacuity for some constructs. Simulators will
        probably not even implement more complex forms anyway.
John: We know that the property implies operator is broken and will need
        to be fixed if it remains in the standard.

Anupam: In the reporting section (40.5.3, p.1053). Doesn't include vacuous
        fail reporting. Will this need to be updated too?
John: Have some concerns on this section.
        Concerned that successes are partitioned into vacuous and non-vacuous
        Fails not partitioned yet.
John: Maybe we just get rid of vacuity. Just talk about success & fails.
Ed: Successes would be all successes, vacuous and non-vacuous
John: With a partial definition: you have to be careful what you require.

Meeting adjourned.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.