Minutes from SV-AC Meeting

Date: 2010-11-02

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=2945761

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

v[xxx-xxxxxxxxxxxxx-] Eduard Cerny (Synopsys)

v[xxxxx-xxxxx-xxxxxx] Ben Cohen

n[x-x-xxx-x--xxxxxxx] Surrendra Dudani (Synopsys)

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

v[xx-xxxx-x-xxxxxxxx] John Havlicek (Freescale)

v[x-xxx-xxxxxxxxxxxx] Tapan Kapoor (Cadence)

t[x--xxxxxxxxxxxxxxx] Dmitry Korchemny (Intel - Chair)

v[x--xxxxxx-xxxxxxxx] Scott Little (Freescale)

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

v[xxxxxxxxxxxxxxxxxx] Anupam Prabhakar (Mentor Graphics)

v[xx-xx--xxxxxxx-xxx] Erik Seligman (Intel)

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

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

|- attendance on 2010-10-26

|--- voting eligibility on 2010-10-26

Agenda:


- Reminder of IEEE patent policy.

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

- Minutes approval

Erik: Move to approve the minutes.

Ben: Second

Vote results: 9y/0n/0a.

- Email ballot results

All issues (2904, 3135, 2412) have unanimously passed. There were friendly amendments. Dana will notify when the friendly amendments have been implemented.

Erik: Issue 2412: Should we allow pass sequence.triggered to an input port to a module?

John and Anupam: Find it helpful

Erik: Then probably an example is needed in the LRM.

- New issues

- Enhancement progress update

2328: Review and relax restrictions on data types in assertions.

Scott: Should we cut the section "(or preserve no state information)" in 16.6? Should a static function without automatic variables be allowed in assertion boolean expressions? If we disallow it, should backward compatibility issues arise? Will send an email describing the problem.

John: Another issue: how far to relax the restriction on boolean expressions? Should we allow unbounded data types such as strings, references to dynamic arrays?

Scott: Queues?

John: Unbounded types may introduce inconsistency between simulation and formal verification.

Ed: dequeue, sampling may be difficult to define. What if an element does not exist?

Anupam: Should dynamic values be sampled?

John: Dynamic variable update may follow regular sampling semantics.

Scott: Only time and realtime are not sampled.

Dmitry: The situation with unbounded data types is similar to procedural concurrent assertions.

Surrendra: Dynamic variables may not yet exist in the Preponed region.

Dmitry: Are there any important use cases justifying our work on it? If not, we can disallow it, and reopen this issue when required.

Ben: This may be useful for local variables.

Surrendra: Agree with Dmitry. The unbounded data types may disallowed for a while.

John: Useful for local variables working as queues.

Ed: Local variables are not sampled. Maybe to bound queues to local variables only?

John: May be useful in any case, such as variables in modules or checkers.

Ed: What about dequeues?

Scott: May consider them as functions with a side effect, and therefore they are disallowed.

Dmitry: We need to prioritize the issues to work on.

3213: Update definition of sampled value

Dmitry: The initial version of the proposal is ready. Need to assign reviewers.

Erik, Anupam: Will review.

3206: Deferred assertions are sensitive to glitches

Dmitry: As Manisha mentioned this issue will arise also when defining the simulation semantics of continuous assignments to checker variables: in the deferred assertion mixes checker and design variables there will be false negatives.

Dmitry: I can think of two approaches: mature deferred assertions in the Postponed region, or to require at least one full loop, so that the deferred assertions are matured at the second visit of the Observed region. If deferred assertions are matured in the Postponed region how can action blocks interact with the design? What is worse, deferred assertion completion will not be visible to the VPI?

Anupam: Workaround could be used: always assign deferred assertion expression in checkers to a shadow variable.

Dmitry: Users won’t like that. Also the problem exists even outside the checker context.

Dmitry: Will send an email describing the problem to SV-AC and SV-BC to initiate discussion.

Vacuity:

Dana presented her document describing different approaches to vacuity definition.

Meeting adjourned.

Topic revision: r1 - 2010-11-12 - 20:02:25 - ErikSeligman
 
Copyright © 2008-2025 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback