Date: 2010-07-27

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

Agenda:

- Reminder of IEEE patent policy.

See: http://standards.ieee.org/board/pat/pat-slideset.ppt

- Minutes approval

- Email ballot results

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

2491: Conflicting rules in 16.17 (D7)

2479: Annex F.5.2.1 conflicts with changes from 2434

3147: Rule c) in 16.17 conflicts with the relaxed rules on clocking of assertions with inferred leading clocking event.

- Issue resolution/discussion

1756: The LRM does not indicate how the control tasks $asserton/off/kill affect verification statements in initial blocks

1763: The LRM does not define whether assertion control tasks affect sequence methods and events

1853: BNF for calls to $rose and other sample value system functions.

2485: terminology related to immediate and deferred assertions.

2558: Restriction inside checker construct

2452: No vacuity information about synchronous aborts

2904: Clarify when disable iff condition must occur relative to starting and ending of an attempt

3134: sequence and property range parameters are erroneously defined

3135: Verbal explanation of nexttime and always is misleading for multiple clocks

2871: Clause 16 does not forbid assertion local variables within clocking event expressions

2353: 'classes' missing from description

1678: Clarify that rewriting algorithm doesn't replace name resolution

2571: confusing assertion clock inference rule

2386: Rename 16.9 to "Local variables"?

- Enhancement progress update

- Opens

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[-xxx] Laurence Bisht (Intel)

v[xxx-] Eduard Cerny (Synopsys)

v[xxxx] Ben Cohen

v[xxxx] Surrendra Dudani (Synopsys)

v[xxxx] Dana Fisman (Synopsys)

v[xxxx] John Havlicek (Freescale)

v[xxxx] Tapan Kapoor (Cadence)

t[xxxx] Dmitry Korchemny (Intel ¿ Chair)

v[xxxx] Scott Little (Freescale)

v[xxxx] Manisha Kulshrestha (Mentor Graphics)

v[xxxx] Anupam Prabhakar (Mentor Graphics)

v[-xxx] Erik Seligman (Intel)

v[xxx.] Samik Sengupta (Synopsys)

v[-xxx] Tom Thatcher (Sun Microsystems ¿ Co-Chair)

|- attendance on 2010-07-27

|--- voting eligibility on 2010-07-27

Minutes

1. IEEE Patent policy: Attendees were reminded.

2. Minutes from last meeting:

Ed: Move to approve minutes

Tapan: Second

voting results: 10y, 0n, 0a

3. E-mail ballot results:

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

Failed.

Will be discussed when Erik returns.

3147: Rule c) in 16.17 conflicts with the relaxed rules on clocking of assertions with inferred leading clocking event.

Ed: Requires to define the notion of maximal property first then objections may be removed.

John: This is a chicken and egg problem.

Ed: Maximal property is what remains after expansion, no clock flow definition required.

Dmitry: If the property is recursive, direct expansion won't work.

Ed: Avoid referencing maximal property?

Ben: Need an example.

2491: Conflicting rules in 16.17 (D7)

Passed: 9y/0n/0a (no change required).

2479: Annex F.5.2.1 conflicts with changes from 2434

Passed: 9y/0n/0a

4. Open Mantis items

1756: The LRM does not indicate how the control tasks $asserton/off/kill affect verification statements in initial blocks

Call to email vote to resolve as "no change required".

2871: Clause 16 does not forbid assertion local variables within clocking event expressions

2353: 'classes' missing from description

Call to email vote.

Attempt definition in case of future value functions.

Ed, Surrendra: A posteriori reporting is not efficient. Also in VPI.

Manisha: Especially $asserton/off

Dmitry: $asserton/of should be consistent with aborts, and aborts cannot be delayed.

John: And other temporal operators, such as until.

Surrendra: $asserton/off support becoming very inefficient for all assertions

Dmitry: Formal semantics cannot be changed. In other cases alternative implementation may be considered.

(To be continued).

5. Enhancements

Real type support in assertions: Scott will update next week.

Output arguments in checkers.

Dmitry: Need to define the simulation semantics of continuous and blocking assignments in checkers. Reconsider the definition of checker variable sampling.

2412 – Clock inference in sequences.

Anupam: What is the reason not to allow default clock inference in assertions?

Ed: Should be consistent with sampled value functions, and there is no inference there.

Anupam: We need allow inference everywhere.

Dana: Why not to infer the assertion clock in these cases?

Dmitry: The users may be confused. It is safer not to do any inference in this case, event though it may look inconsistent.

Proposal will be updated and discussed by email