SV-ACMinutes2010_09_07 < P1800

P1800 Web>SystemVerilogAssertionCommittee>SVACMeetingMinutes>SV-ACMinutes2010_09_07 (2010-09-16, ErikSeligman) (raw view)EditAttach
Minutes from SV-AV Committee Meeting

Date: 2010-09-07

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

- New issues

3195: Local Variables Flow Out Issue in and/or/intersect/implies

- Issue resolution/discussion

1853: BNF for calls to $rose and other sample value system functions.

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

1678: Clarify that rewriting algorithm doesn't replace name resolution

2571: confusing assertion clock inference rule

2386: Rename 16.9 to "Local variables"?

3117: make it clear that rewriting algorithm (F.4.1) applies to checker

and let

- Enhancement progress update

Checker usability enhancements

- 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[xxxxx--xxx] Laurence Bisht (Intel)

  v[xxxxxxxxx-] Eduard Cerny (Synopsys)

  v[xxx-xxxxxx] Ben Cohen

  v[x--xxxxxxx] Surrendra Dudani (Synopsys)

  n[x---x-xxxx] Dana Fisman (Synopsys)

  v[x-xxxxxxxx] John Havlicek (Freescale)

  v[xxxxxxxxxx] Tapan Kapoor (Cadence)

  t[xxxxxxxxxx] Dmitry Korchemny (Intel ¿ Chair)

  v[x-xxxxxxxx] Scott Little (Freescale)

  v[xx-xxxxxxx] Manisha Kulshrestha (Mentor Graphics)

  v[xxxxxxxxxx] Anupam Prabhakar (Mentor Graphics)

  v[xxxxxx-xxx] Erik Seligman (Intel)

  v[x-xxxxxxx.] Samik Sengupta (Synopsys)

  v[xxxxxx-xxx] Tom Thatcher (Oracle ¿ Co-Chair)

    |- attendance on 2010-08-31

  |--- voting eligibility on 2010-08-31

Minutes:

--------

- Reminder of IEEE patent policy.

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

- Minutes approval

Tom: Made two corrections to minutes:

Erik: Move to approve minutes.

Scott:     Second

vote results   0n 0a

New Issues

----------

Ben: Proposed 3195

     Graphical representation of requirement requires modeling of

     concurrent processes, which would need to share data.

     Allows concurrent approach, as opposed to a forward approach.

     IN current SVA always go forward (w exception of AND/intersect)

John: Do you intend to always initialize the local variable?

Ben: Yes

Ben  This proposal is to allow describing property in timing diagram.

     Multiple processes contribute to requirement

Ed:  Do assertion attempts overlap?

Ben  Only change is allowing flow-in of local variable to sub-properties.

Ed:  Do you need local variable for that, or would a global variable work?

Ben: Need a local variable.

Ben: Lot of text in standard dealing w/ Flow out from AND/OR/Intersect

     Flow in not addressed in standard.

John: There are two places discussing flow-in Clause 16, Annex F.

     Main point: How should variable be shared?

     You are asking for variable to be shared among all sub-properties

     for a given attempt?

Ben: Restrictions: only one sub-property can write. Can't write & read

     in same cycle.

Ed:  You could add semaphores.

Ben: That would add more complexity.

Ed:  Without semaphores, might not be able to evaluate statically.

Ben: Is there interest in this?

Ed:  This may go beyond current PAR.

Dmitry:    Suggest we discuss next time what other enhancements we would like

     the working group to approve.

Dana: Looking at example. It looks like it could be represented in PSL.

Ben: I think it is the forall in PSL that allows this.

Dmitry:    May be able to use const free variables to do this.

Ed:  Good for formal, Not good in simulation

John: Depending on what the tool does, use of const formal may not get a

     meaningful evaluation.

Issue Resolution

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

2452:

Dana: Just added two conditions to the vacuity for sync_accept_on and

     sync_reject_on

Dmitry:    Will call for an e-mail vote

Dmitry:    In proposal, new text should be in blue.

Ed:  Should text read "clock event", or "clocking event"?

Dmitry:    Should be "clocking event".

Manisha: So if property fails because of reject-on, that means it is

vacuous?

     Is that what we want?

     If section discussing sync_accept_on, if abort conddition true, it is

     a successful evaluation.

Dmitry:    Successful, and vacuous

2904:

Anupam: For single clock properties, I don't see why it would be needed.

     For multi-clocked it might be useful.

Dmitry: Don't see why multiple clocks should affect this

Tapan:     page 318:

Tom: Is it possible for disable condition to change in Observed region?

Dmitry:    If $triggered is called in disable condition, then disable could

     become true in the Observed region.

Manisha: What about accept_on/reject_on?

Ed:  Evaluated in observed region, using sampled values.

Tom: Main difference seems to be ending of evaluation: Before, if disable

     condition became true in the Observed region, it seems that it depended

     on event ordering whether a property evaluated true or false or

     disabled. Now, it wil always evalutate to disabled.

Samik Maybe define it like this? If evaluation ends in the Observed region

     of a time step. and disable condition has not occurred by the

     beginning of the Observed region, then disable won't affect the result.

Anupam: Can we get an example where there is a confusion?

John: There was one in the Mantis item in the description

     In example: The disable condition is the clock. The clocking

     event of the property is @(negedge clk)

John: Intuition was that property was not disabled.

Tapan:     Don't see why this is not defined by current text.

     Evaluation begins in observed region, clock is already 0.

Ed:  LRM doesn't say anything. That's why clarification was requested.

Tapan:     On @(negedge) of clock, clock is 0 by the time Observed region

     begins.

John: Value of clock in Observed region is 0. But it would have been 1 at

     some time prior in same the time step. Question is: Does this

     affect the property evaluation.

Tom: Seems like at the beginning time step of the evaluation there is no

     change. It's just a clarification. However, at the final time step

     of the evaluation, there seems to be a change. If disable condition

     occurs during Observed region, in current LRM the event ordering

     determines whether property evaluates to true or false, or disabled.

     With this proposal, a property cannot evaluate to true or false until

     it's disable condition has been evaluated.

John: We should think about that.

John: We already have ordering problems, if $triggered is called within a

     sequence/property evaluation, it must be evaluated first.

Enhancements

----------

Dmitry:    Would like to organize face-to-face in November

Ed:  Travel justificaiton would be an issue.

Dmitry:    We could hold it in Silicon Valley so a minimum number of people

     need to channel.

Dmitry:    Let's discuss it next time.

Checker Sampling:

Dmitry:    E-mail ballot last week on 3035 failed.

Dmitry:    Wrote up a document describing need for change.

Dmitry: Believe that everyone agrees that checker formal arguments should

     not be automatically sampled at the checker interface. They should

     be sampled based on the context where they appear in code.

Ben: Interfaces?

Dmitry:    Should be OK, because it doesn't affect the definition.

John: Main problem with Mantis proposal was that rules for various contexts

     were not defined.

Dmitry:    e.g. Variables are sampled when they appear in concurrent assertion.

John: Would we need to use $sampled in the checker?

Dmitry:    Some contexts would be sampled, some not sampled. Could use

$sampled

     if you need variable to be sampled.

John: Reasonable. Manisha has already pointed out that current method

     is breaking re-writing rule.

Dmitry:    Proposal: Within concurrent assertions, some things sampled,

some not:

     Automatic variables, $triggered, free variables not sampled.

Dmitry: Will discuss document more next week.

Meeting adjourned.
Topic revision: r1 - 2010-09-16 - 22:23:42 - ErikSeligman
P1800