[sv-ac] Minutes from SV-AC meeting 07/27/2010

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
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.