[sv-ac] SV-AC meeting minutes, 2009-05-26

Minutes of IEEE P1800 SV-AC meeting #2009-06



Date:  2009-05-26

Time:  16:00 UTC (09:00 PDT)



Dialin information:

-------------------

Toll number:   +1 916-356-2663

Toll free number (US): 888-875-9370 (U.S. toll-free),

Bridge: 2 Passcode: 9296766


Attendance Record:
------------------
        Legend:
               x = attended
               - = missed
               r = represented
               . = not yet a member
               v = valid voter (2 out of last 3 or 2/3)
               n = not a valid voter
               t = chair eligible to vote only to make or break a tie

Attendance re-initialized on 2009-04-13:

v[xx-xxx] Doron Bustan (Intel)
v[--xxxx] Eduard Cerny (Synopsys)
v[xxxx-x] Ben Cohen
v[xxx--x] John Havlicek (Freescale)
v[xxx-xx] Tapan Kapoor (Cadence)
t[xxxxxx] Dmitry Korchemny (Intel - Chair)
v[-xx-xx] Manisha Kulshrestha (Mentor Graphics)
v[xxx-x.] Lisa Piper
v[x-xxxx] Erik Seligman (Intel)
v[xxxxxx] Bassam Tabbara (Synopsys)
v[xxxx-x] Tom Thatcher (Sun Microsystems - Co-Chair)
  |-------------- attendance on 2009-05-26
|---------------- voting eligibility on 2009-05-26



Agenda:

-------



- Reminder of IEEE patent policy.

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



- Approve meeting minutes from 2009-05-04.

Erik moves.

Tom seconds.



Motion passed 8y/0a/0n.



- Discuss Mantis item 2659:

 Backward compatibility issue with sequence property.



Tapan: Need to keep the definition of sequential property backward compatible. In the LRM 2005 sequential properties are strong, and in the LRM 2009 they will become weak by default in assertions and assumptions.



John & Dmitry: The behavior of strong sequential properties is counterintuitive in boolean assertions: you have to check for clock fairness. No tools are known that enforce clock fairness checking, and therefore the semantics of strong properties is violated in implementations. A reasonable compromise is to allow change the semantics to be consistent with implementations in most cases, and to make it non-backward compatible for a small fraction of use cases.



John: Additional reason to keep semantics aligned with PSL.



Tapan agrees with the first statement and disagrees with the second.

Tapan: Need to publish the motivation in the LRM.



Tom & Dmitry: It is not appropriate to publish the motivation in the LRM.



Erik: It may be published separately, e.g., in DVCon proceedings.



John suggest to publish the explanation at least in the reflector.

Action item: John will compose the explanation.



John moves to approve the resolution of Mantis 2659.

Doron seconds.



Motion passed: 8y/0a/0n.





- Opens.



Ben: Two open issues: clock change in if property (Mantis 2754) and allow checker formal arguments to be connected to interfaces (Mantis 2751).



Dmitry: In the LRM 2009 it is allowed to change the clock in if properties. LRM examples are also correct, though they might be made clearer.



Tom: Agree about usefulness of connecting checker arguments to interfaces, but the checker is a new construct, and it was infeasible to analyze all implications of these extensions, and it was decided to keep only very basic features in checkers and to add new features in next releases.

---------------------------------------------------------------------
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.