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.