SV-ACMinutes2010_10_26 < P1800

P1800 Web>SystemVerilogAssertionCommittee>SVACMeetingMinutes>SV-ACMinutes2010_10_26 (2010-11-01, ErikSeligman) (raw view)EditAttach
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.
Topic revision: r1 - 2010-11-01 - 19:22:28 - ErikSeligman
P1800