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.