SV-ACMinutes2010_10_12 < P1800

P1800 Web>SystemVerilogAssertionCommittee>SVACMeetingMinutes>SV-ACMinutes2010_10_12 (2010-10-15, ErikSeligman) (raw view)EditAttach
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.
Topic revision: r1 - 2010-10-15 - 20:17:21 - ErikSeligman
P1800