Date: 2010-11-23

Time: 16:30 UTC (8:30 PST)

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

Agenda:

- Reminder of IEEE patent policy.

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

- Minutes approval

- Email ballot results

None

- New issues

None

- Issue resolution/discussion

Addressing champions' feedback.

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

v[xxxxxx-xxxxxxxxxxxxx-] Eduard Cerny (Synopsys)

v[-xxxxxxx-xxxxx-xxxxxx] Ben Cohen

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

n[x--xx---xxxx---x-xxxx] Dana Fisman (Synopsys)

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

v[xxxx-xxx-xxxxxxxxxxxx] Tapan Kapoor (Cadence)

t[xxxx--xxxxxxxxxxxxxxx] Dmitry Korchemny (Intel ¿ Chair)

v[xxxx--xxxxxx-xxxxxxxx] Scott Little (Freescale)

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

v[x-xxxxxxxxxxxxxxxxxxx] Anupam Prabhakar (Mentor Graphics)

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

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

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

|- attendance on 2010-11-23

|--- voting eligibility on 2010-11-23

Minutes:

- Reminder of IEEE patent policy.

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

Participants were reminded of the IEEE Patent policy

- Minutes approval

Erik: Move to approve minutes

Scott: Second

Vote results: 10y, 0n, 0a

- Issue resolution/discussion

Addressing champions' feedback.

3168: Shalom suggests we close this as a duplicate of 3008

Scott: Sounds fine (Scott originally entered the Mantis item)

Scott: Move to resolve 3168 as a duplicate of 3008

Samik: Second

Vote results: 10y, 0n, 0a

2291: the description of $assertoff blurs assertions and attempts

Laurence: Uploaded a new proposal to address champions

Samik: Should sentence read "no new attempt" (singular)?

Erik: It's fine as written

Erik: Move to accept proposal for 2291.

Scott: Second

Vote results: 10y, 0n, 0a

2330: Clarify that number_of_ticks argument to $past must be

compile-time constant

John: Hasn't updated proposal yet

Laurence: Should we change BNF to show requirement?

i.e. Create a BNF for compile-time constant

Dmitry: Currently it's not necessary.

Would be a major change.

(Dana Joined)

Tom: If we were to change BNF, it should be done under a separate Mantis

Dmitry: There is a mantis item 3113 which addresses a similar issue

Postpone to next meeting

2387: Layout of 16.11 is inconsistent

Erik: Hasn't updated proposal yet. Didn't get notice.

2552: Confusing comments regarding nexttime operator

Dmitry: Has updated the proposal:

Dmitry: Added text specifying requirement that weak eventually have a

bounded

Range.

John; Would this make previously working code not compile?

Manisha: Change is good to have

Tom: Example: unbounded range on weak eventually, might currently compile,

but would never fire. With change, this code would have a compile-

time error

Manisha: But BNF already specifies bounded range.

Dmitry: Will call for an E-mal vote.

2557: Rules for passing automatic variables to sequence subroutines are

not clear

Manisha: Could delete part about constant input.

Manisha: An automatic is always a constant input, it's not an option.

Erik: Will update proposal

2722: Errors in Figures 16-14, 16-15, and 16-16

Tom: Proposal uploaded. Only change was to change inserted text from

blue underlined text to blue.

Laurence: Should figure reference be underlined?

Anupam: It's underlined in in the LRM.

Tom: Move to accept proposal for 2722

John: Second

Vote results: 10y, 0n, 0a

2804: Need to clarify rule (b) in 16.15.6 to allow inferred clock when

expression appears in procedural assertion

Erik: Has posted detailed response to John's concerns

John: Has not read the response.

Erik and John will discuss John's concerens

Erik Will clarify with Francois what her concerns were.

2839: Contradictory statement of increment/decrement operators usage.

Objection from champions was that was "design variables" was not

defined

John: Suggest to remove last sentence altogether.

Assertions do have side effects.

Tom: Could rephrase "This restriction prevents side effects on variables

referenced by assertion expression"

Ed: Should I fix lvalue as well?

Champions complained about the use of undefined term "lvalue" on

some other proposal.

If we eliminate that term in other proposals, we should elimintate

it here.

Ed: Anupam's suggestion: Replace "lvalue" with "modified operand"

OK?

John: OK with me.

John: variable_lvalue is a BNF non-terminal, this term appears elsewhere

in this section, and it does appear in the BNF for these operators.

Manisha: Would prefer to use variable_lvalue.

Ed: Will update

- Enhancement progress update

Vacuity definition (Dana¿s presentation)

Dana: Presented her document on Vacuity definitions.

Suggest that we settle on

John: Don't understand TAF (Temporal Antecedant Failure) definition of

Vacuity. How would it behave with a contrapositive

p |-> q

~q |-> ~p

Does TAF treat them the same?

Dana: Yes. Think of an automation which is checking a property

Equivalent properties would have equivalent automaton.

Notion of temporal is the same

Scott: p |-> q would suffer from TAF if p is always false.

But ~q |-> ~p would not, correct?

Maybe make the example temporal, that would help to clarify.

Dmitry: Suggest we have a brainstorming session on vacuity.

Back to 2839:

Ed has updated proposal.

John: Move to accept 2839

Ed: Second

Vote results: 10y, 0n, 0a

Continuous assignments in checkers

Dmitry: Summarized e-mail discussion.

Meeting Adjourned