Date: 2010-10-12

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=9261632

Agenda:

- Reminder of IEEE patent policy.

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

- Minutes approval

- Issue resolution/discussion

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

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

v[-xxxxxxxxxxxxx-] Eduard Cerny (Synopsys)

v[xx-xxxxx-xxxxxx] Ben Cohen

v[-xxx-x--xxxxxxx] Surrendra Dudani (Synopsys)

v[--xxxx---x-xxxx] Dana Fisman (Synopsys)

v[xxxx-x-xxxxxxxx] John Havlicek (Freescale)

v[-x-xxxxxxxxxxxx] Tapan Kapoor (Cadence)

t[xxxxxxxxxxxxxxx] Dmitry Korchemny (Intel ¿ Chair)

v[xxxxxx-xxxxxxxx] Scott Little (Freescale)

v[xxxxxxx-xxxxxxx] Manisha Kulshrestha (Mentor Graphics)

v[xxxxxxxxxxxxxxx] Anupam Prabhakar (Mentor Graphics)

v[xx--xxxxxxx-xxx] Erik Seligman (Intel)

v[xxxxxx-xxxxxxx.] Samik Sengupta (Synopsys)

v[xxxxxxxxxxx-xxx] Tom Thatcher (Oracle ¿ Co-Chair)

|- attendance on 2010-10-12

|--- voting eligibility on 2010-10-12

Minutes:

- Reminder of IEEE patent policy.

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

Participanats were reminded of the policy.

- Minutes approval

Erik: Move to approve minutes

Samik: Second

Voting Results: , 0n, 0a

- Issue resolution/discussion

2328 - Review and relax restrictions on data types in assertions

Scott: Need to get a new proposal together. When it is done, will send it

out.

- Enhancement progress Update

Vacuity discussion:

Ben: Had created a modification of Scott's table.

Ben: If antecedant is false, why do we care if property vacuous or not

Scott: Think that you need to separate true/false from vacuous/nonvacuous

Ben: Does a vacuous false mean a less important failure?

Dmitry: No, you can't ignore failure even if vacuous false.

John: Although standard may distinguish betwee vacuous and non-vacuous

failure, the end-user doesn't need to. User may want to see all

failures, and doesn't care about vacuous fail vs non-vacuous fail.

But

Ben: In formal verification: does it make any difference?

Ben: a implies b implies c: Which is evaluated first?

John: Believe it is right associative.

The order of evaluation is not important to this issue. Can always

add parenthesis.

Tom: Is this document talking specifically about the property implies

operator, or is it about implication in general?

Scott: Document talks about property implies?

Tom: So the document is proposing two new possible definitions of

vacuity for a property implies?

Scott: Current definition in LRM is broken (implies0 in document). The

implies1 and implies2 are two possible suggestions for a fix.

A property implies will have cases not seen by sequence implication

operators.

Manisha: What is difference between implies1 and implies2

John: The implies2 definition requires non-vacuity of antecedant.

John: Suggest that we don't try to decide now. Were there any other points.

Ben: Would like to converge. Think that a table in the LRM would make

things much clearer

Dmitry: A table would need to go in an annex.

Ben: Don't care where the table is. Think that a table would make this

much clearer.

Could vacuity for implies be defined in terms of vacuity of

property

or operator?

John: Vacuity for implies is not symmetric. Would be suspicious of any

vacuity definition for property or that was not symmetric.