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.