SV-ACMinutes2010_08_31 < P1800

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

Date: 2010-08-31

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

Issue 2571 passed: 11y/1a/0n

Issues 2205 and 3035 failed

- New issues

3191: Allow sequence methods with sequence expressions

- Issue resolution/discussion

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

and let

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"?

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

  v[xxxxxxxx-] Eduard Cerny (Synopsys)

  v[xx-xxxxxx] Ben Cohen

  v[--xxxxxxx] Surrendra Dudani (Synopsys)

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

  v[-xxxxxxxx] John Havlicek (Freescale)

  v[xxxxxxxxx] Tapan Kapoor (Cadence)

  t[xxxxxxxxx] Dmitry Korchemny (Intel ¿ Chair)

  v[-xxxxxxxx] Scott Little (Freescale)

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

  v[xxxxxxxxx] Anupam Prabhakar (Mentor Graphics)

  v[xxxxx-xxx] Erik Seligman (Intel)

  v[-xxxxxxx.] Samik Sengupta (Synopsys)

  v[xxxxx-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

Participants were reminded of the IEEE patent policy

- Minutes approval

Erik: Move to approve minutes

Ed:  Second

     Vote results: 7y, 0n, 0a

- Email ballot results

Issue 2571 passed: 11y/1a/0n

Issues 2205 and 3035 failed

2205: Failed with one negative vote.

Lawrence: What about expect

Dmitry:      The expect construct is not included in "assertion_statement"

Erik: Move to approve proposal for 2205

Lawrence: second

     Vote results: 7y, 0n, 0a

3035: Failed with negative votes from Tom, John, and Scott

Tom: Checker formal argument would be sampled when used on RHS of an

     assignment, but not sampled when used in a deferred assertion.

Ed:  Checker variables assigned in re-NBA, so need to be sampled.

     Free Variables assigned values at beginning of Observed

Anupam:

     Are checker variables and free variables sampled when on RHS?

        In proposal "counter is a checker variable, and therefore not

sampled"

Ed: Checker formals and design variables (by xmr) would be sampled if on

     the right side of a checker

Ed: Don't make distinction between design and checker variables.

     Free variables init at observed:

Anupam: Since we are going to add other constructs,

    Probably easier to say what is not sampled.

     Anything in an event control is not sampled.

     What if we added an "if" construct? Would variables in "if" be

     sampled?

Ed: Should be sampled.

Manisha: We do have $sampled system function. We could make everything

     not sampled by default, and just have the user use $sampled where it

     is needed

Dmitry: But this would not be convenient

Ed:  In OVL they don't use sampled. But they do sample using cont assign

     Manisha's idea does make things more consistent.

     It's more awkward, but semantics are consistent

Manisha: If it's difficult to remember where variables are sampled, and

where

     they are not sampled, it would be better to require the user to

     specify.

Ed:  What if we had a $default_sampling system function. This woule allow

     user to specify at the beginning which variables are sampled inside

     the checker.

Ed:  If I use a checker variable assigned with continuous assignment,

    would that still be sampled?

     Still need to solve randomization of free variables.

Dmitry:    Variable on rhs of continuous assignment should not be sampled.

Ed:  What about combinational always blocks: This would be like a

     continuous assignment.

Dmitry: In conditional always, we don't want the RHS variables to be

sampled.

Dmitry: Maybe we should define sampling by procedure, not by statements?

Ed:  Would we annotate the procedure as to whether it uses sampled

     variables or not?

Dmitry:    No, define rules like "@posedge clk procedures are sampled,

     always_comb procedures are not sampled"

Lawrence   What about a checker instantiated within an always block?

     Would this change the sampling semantics at all?

Ed:  How do we determine which always blocks are procedural, which are

     combinational?

Dmitry: In always_comb, no sampling, in always @(clk) sampling

Dmitry: The "if" construct: within always_comb, variables in the "if"

     expression are not sampled. In an always @(clk), these variables

     would be sampled.

Dmitry: Checkers typically written by verification people. It may be more

     difficult to write, but should be easy to use.

Dmitry: We can postpone this proposal,

    Can we at least agree that checker formal arguments are not sampled,

     but will be sampled according to how they are used in context.

Manisha: Sampling of checker formal arguments is breaking the re-writing

     algorithm.

Dmitry:    Single-assignment-rule: This should apply to continuous assignments

     as well.

Ed:  We should limit scope for now to checkers with current limitations,

     plus continuous assignments. We can deal with the effect of other

     constructs later.

Dmitry:    Will send out a summary of ideas for resolution of checker sampling

     we will discuss next week, before writing new proposal.

New Issues

----------

3191: Allow sequence methods with sequence expressions

Dmitry: An enhancement: we would need to get approval to work on it.

Issue Resolution:

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

2476

Erik: Want to make $onehot, $countones available outside assertions

Erik: What about time sensitive functions $past, $sampled, etc

Ed:  Already allowed outside functions see page 400

Erik: What about global clocking functions

Dmitry:    Not allowed outside assertions

Dmitry:    We should allow the global clocking functions in let

Ed:  If you allow them in Let, then you have to restrict where the let

     may be used.

Erik: Let contents are substituted where they appear. Wouldn't

     restrictions on let contents already be covered by existing rules?

Erik: Should we allow global clocking past functions?

Ed:  Even section 20 should be corrected?

Erik In20.13 wierd BNF construct assert_boolean

Ed:  Don't know if sampled value functions are allowed in classes.

     May be only allowed in static variables.

Erik: Will work on an proposal

Enhancement Discussion

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

INterfaces

Ben: Wrote up use cases for interfaces

     with modports, clocking blocks

     Wrote up models:

     used module in place of checker for simulation purposes

     What issues will come up when adding this to checkers?

     Would tasks defined within interfaces be allowed?

Meeting adjourned.
Topic revision: r1 - 2010-09-02 - 22:04:31 - ErikSeligman
P1800