[sv-ac] Minutes of SV-AC Meeting

Minutes from SV-AC Meeting
Date: 2010-10-12
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=9261632

Agenda:
-------
- Reminder of IEEE patent policy.
See: http://standards.ieee.org/board/pat/pat-slideset.ppt

- Minutes approval

- Issue resolution/discussion
2328 - Review and relax restrictions on data types in assertions
2904 - Clarify when disable iff condition must occur relative to
starting and ending of an attempt
3135 - Verbal explanation of nexttime and always is misleading for
multiple clocks

- 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[xx-x-xxxxx--xxx] Laurence Bisht (Intel)
   v[-xxxxxxxxxxxxx-] Eduard Cerny (Synopsys)
   v[xx-xxxxx-xxxxxx] Ben Cohen
   v[-xxx-x--xxxxxxx] Surrendra Dudani (Synopsys)
   v[--xxxx---x-xxxx] Dana Fisman (Synopsys)
   v[xxxx-x-xxxxxxxx] John Havlicek (Freescale)
   v[-x-xxxxxxxxxxxx] Tapan Kapoor (Cadence)
   t[xxxxxxxxxxxxxxx] Dmitry Korchemny (Intel ¿ Chair)
   v[xxxxxx-xxxxxxxx] Scott Little (Freescale)
   v[xxxxxxx-xxxxxxx] Manisha Kulshrestha (Mentor Graphics)
   v[xxxxxxxxxxxxxxx] Anupam Prabhakar (Mentor Graphics)
   v[xx--xxxxxxx-xxx] Erik Seligman (Intel)
   v[xxxxxx-xxxxxxx.] Samik Sengupta (Synopsys)
   v[xxxxxxxxxxx-xxx] Tom Thatcher (Oracle ¿ Co-Chair)
     |- attendance on 2010-10-12
   |--- voting eligibility on 2010-10-12

Minutes:
--------
- Reminder of IEEE patent policy.
See: http://standards.ieee.org/board/pat/pat-slideset.ppt
Participanats were reminded of the policy.

- Minutes approval
Erik: Move to approve minutes
Samik: Second
Voting Results: , 0n, 0a

- Issue resolution/discussion
2328 - Review and relax restrictions on data types in assertions
Scott: Need to get a new proposal together. When it is done, will send it
        out.

- Enhancement progress Update

Vacuity discussion:
Ben: Had created a modification of Scott's table.

Ben: If antecedant is false, why do we care if property vacuous or not
Scott: Think that you need to separate true/false from vacuous/nonvacuous

Ben: Does a vacuous false mean a less important failure?
Dmitry: No, you can't ignore failure even if vacuous false.

John: Although standard may distinguish betwee vacuous and non-vacuous
        failure, the end-user doesn't need to. User may want to see all
        failures, and doesn't care about vacuous fail vs non-vacuous fail.
        But
Ben: In formal verification: does it make any difference?

Ben: a implies b implies c: Which is evaluated first?
John: Believe it is right associative.
        The order of evaluation is not important to this issue. Can always
        add parenthesis.

Tom: Is this document talking specifically about the property implies
        operator, or is it about implication in general?
Scott: Document talks about property implies?
Tom: So the document is proposing two new possible definitions of
        vacuity for a property implies?
Scott: Current definition in LRM is broken (implies0 in document). The
        implies1 and implies2 are two possible suggestions for a fix.
        A property implies will have cases not seen by sequence implication
        operators.

Manisha: What is difference between implies1 and implies2
John: The implies2 definition requires non-vacuity of antecedant.
John: Suggest that we don't try to decide now. Were there any other points.
Ben: Would like to converge. Think that a table in the LRM would make
        things much clearer
Dmitry: A table would need to go in an annex.
Ben: Don't care where the table is. Think that a table would make this
        much clearer.

         Could vacuity for implies be defined in terms of vacuity of
property
        or operator?
John: Vacuity for implies is not symmetric. Would be suspicious of any
        vacuity definition for property or that was not symmetric.

Meeting adjourned.

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