Minutes from SV-AC Committee Meeting

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

Topic revision: r1 - 2010-08-10 - 16:42:35 - ErikSeligman
 
Copyright © 2008-2024 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback