Date: 2010-10-05

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

Agenda:

- Reminder of IEEE patent policy.

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

- Minutes approval

- Email ballot results

- New issues

- Enhancement progress update

- Issue resolution/discussion

Feedback on 2476 and 2205

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

v[xxxxxxxxxxxxx-] Eduard Cerny (Synopsys)

v[x-xxxxx-xxxxxx] Ben Cohen

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

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

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

v[x-xxxxxxxxxxxx] Tapan Kapoor (Cadence)

t[xxxxxxxxxxxxxx] Dmitry Korchemny (Intel ¿ Chair)

v[xxxxx-xxxxxxxx] Scott Little (Freescale)

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

v[xxxxxxxxxxxxxx] Anupam Prabhakar (Mentor Graphics)

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

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

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

|- attendance on 2010-00-05

|--- voting eligibility on 2010-10-05

Minutes:

- Reminder of IEEE patent policy.

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

Participants were reminded of the policy.

- Minutes approval

Erik: Move to approve minutes

Scott: Second

Voting Results: 11y, 0n, 0a

(Surrendra Joined)

- Email ballot results

2386 and 3134 passed.

2328, 2904, and 3135 failed.

3134: Friendly Amendments:

John: Proposal had a red strikeout through a space in the cited text.

Editor would probably miss it.

Removal of space should be a separate change item in the proposal

2328:

Dave Rich's Comment: Removing restriction on non-integer types would also

allow other unexpected types in addition to the intende real types.

Scott: In 16.6: boolean expressions,

Current proposal relaxes restrictions on types of boolean

What is sampled?

Side effects: should be no side effects

Dynamic entities:

Anupam: Agree

John: What other things might be allowed by this approach:

Real expressions, equality of real expressions

C-handle: Does have coersions to integral types already, so wonder

why it is explicity excluded.

Assertions on sizes of arrays might be allowed.

Surrendra: Does proposal suggest to sample dynamic variables.

John: Thought was "yes", but time and event types not sampled

Anupam: How would you use an event in an assertion?

Manisha: Can call triggered() on the event, which returns a boolean.

Manisha: Dynamic arrays: could be large. Sampling the contents of an array

could be expensive.

John & Scott will rewrite the proposal.

2904:

Tapan: New text seems to contradict paragraph on 16.6.

John: It would be a good idea to improve the wording of this

Manisha: Would be a good idea to fix.

John: could delete text after code example.

Or could add "only" to the sentence.

Samik: The point of this paragraph is that disable condition not sampled.

John: Can work with Dana to work on wording.

3135:

Erik: Thought that definitions were incomplete, and that the paragraph was

then needed to to complete definition.

Couldn't the actual definition be completed so the additional

paragraph was not needed?

Erik: Maybe add the text in the explanatory paragraph directly to the

original definitions.

Dmitry: Will ask Dana to make the change.

John: Will this make simple case harder to understand?

Erik: Don't think so.

- New issues

3217 Entered by Surrendra:

"Definition for referring to an assertion as a relative hierarchical

name is missing in Section 23.6"

Tom: How are assertion/property labels different from any other instance

name?

Tom: You can refer to variable names hierarchically.

Erik: Thought that variable names were treated similarly to instance names.

Is there any text which specifies this?

Scott: Has anyone asked sv-bc about this?

Surrendra: Hierarchical references refer to a scope

Label in front of assertion is not a scope.

Needs to be listed in 23.6

John: There are other things not listed that can be referenced

Manisha: In 16.15 "a concurrent assertion can be referenced by its

name"

Surrendra: Think it needs to say something about this in 23.6.

Surrendra: BNF in 23.8: No mention of assertions

Manisha: Block identifier is included in BNF,

Surrendra: Assertion label is a statement label, not a block identifier.

Anupam: How are variables in action block referenced?

John: Will someone on SV-BC be asked to help with this?

-Issue resoluation/discussion

Feedback on 2476 and 2205

Dmitry: Feedback is that 2476 and 2205 are not consistent

Erik: The only contradiction is that 2205 modifies text in 2013 which is

deleted by 2476.

Tom: Only change that needs to be made is to remove the change in 2205

that refers to the section 20.13.

Dmitry: Lets wait for the official Champions ballot.

They will give feedback on what to do.

Erik: Were we going to send to 2476 to SV-BC for comments?

Dmitry: Will wait for champions ballot results.

- Enhancement progress update

Vacuity:

Ben: Created a table for vacuity evaluation for different cases.

Scott: Do tables calculate vacuity for cases? Would like to see

vacuous result even when property fails.

Ben: What is a vacuous fail?

Scott: When property fails, but vacuity returns true.

Tapan: One case would be reject_on, which could fail vacuously

Scott: I have a version of the table, I can send.

Have tables of what LRM says today, and tables of what it should be.

But it's not clear in all cases.

Definition currently is syntactic, not semantic.

"implies" needs to be fixed, but other changes are not so clear.

Erik: Had suggested some method to disable vacuity check for a given

assertion.

Ben: Do your tables cover the case of property AND and OR.

Scott: The tables cover this, but not sure I like the definitions.

e.g. p1 or p2: if p1 passes non-vacuously, and p2 fails vacuously,

The result should be pass non-vacuously: is this correct? Or is

vacuous result of p2 incorrectly ignored?

Meeting adjourned.