Minutes of the sv-sc sub-committee meeting, June 24, 2008

=================Attendance=============================

   21020220 Day
   47306817
   00000000 Month
   66655444
   00000000 Year
   88888888

--[-------a]   Arturo Salz          - Synopsys
vv[aaaa-aa-]   Abigail Morehouse    - Mentor
--[-------a]   Bassam Tabbara       - Synopsys
--[-------a]   Brad Pierce          - Synopsys
--[---a-aaa]   Cliff Cummings       - Sunburst Design
v-[a--aaaaa]   Dave Rich            - Mentor Graphics
vv[aaaaa-aa]   Dmitry Korchemny     - Intel
--[---a-aa-]   Don Mills            -
--[---aaaaa]   Eduard Cerny         - Synopsys
tt[aaaaaaaa]   Erik Seligman        - Intel (chair)
vv[aaaaaaaa]   Francoise Martinolle - Cadence
vv[aaaaaaaa]   Gordon Vreugdenhil   - Mentor Graphics
vv[a-aaaaa-]   Jin Yang             - Intel
vv[--aaaaaa]   John Havlicek        - Freescale
--[-------a]   Jonathan Bromley     - Doulas
--[--a--a-a]   Karen Pieper         - Accellera
vv[aaaaaaaa]   Lisa Piper           - Cadence
vv[-aaaaaaa]   Manisha Kulshrestha  - Mentor Graphics
vv[aaaaaaaa]   Mark Hartoog         - Synopsys
vv[--aaaaaa]   Mehdi Mohtashemi     - Synopsys
vv[aaaaa...]   Michael Burns        - Freescale
vv[--aaaaaa]   Mirek Forczek        - Aldec
vv[--aaaaaa]   Neil Korpusik        - Sun Microsystems
--[------a-]   Ray Ryan             - Mentor
--[------aa]   Shalom Bresticker    - Intel
vv[aaaaaaaa]   Steven Sharp         - Cadence
--[-----aaa]   Stu Sutherland       - Sutherland HDL
--[------aa]   Surrendra Dudani     - Synopsys
vv[aaaaaaaa]   Tom Thatcher         - Sun Microsystems (co-chair)
||
||---- Voting eligibility for current meeting
|------Voting eligibility for next meeting


====================Agenda==============================

Agenda:

   1.  Review the patent policy
   2. Approve the minutes from the last meeting, available at
       http://www.eda.org/twiki/bin/view.cgi/P1800/SvScMeetingMinutes20080617
   3. Overall status: we're running out of time, are we on schedule for these
       action items? Do we need to assign reviewers for current drafts of some?
       (Short scheduling discussion, defer tech discussion until all these are
   visited):
          * 2398: Concurrent Asserts in Procedural Code: New semantics:
       (Erik/Gord) 6/24 to write, 7/8 to pass
          * 2370: $past in Procedural Code (Jin) (6/24)
          * 1900: Checkers: (Dmitry/Erik/Mike/Tom) ETA 7/1 for initial proposal,
       7/15 to pass
          * 2182: VPI Diagrams for Checkers (Chuck Berking) 7/15 to write,
       7/22 to pass
          * 1728: Let Statements (Dmitry) 6/24 to write, 7/1 to pass
          * 1549 update: self-determined types (Gord) 7/1 to write, 7/8 to pass
          * New "@edge clk" proposal (Jin): 7/1 to write, 7/8 to pass
          * New proposal for 'let' VPI (Abi?): 7/1 to write, 7/8 to pass 
   4. Checkers: tech discussion on major unresolved issues, assembled by Dmitry.
          * Checker instantiation semantics ? actual argument typing,
       related to Gord?s proposal (1549). It should be crafted for
       checkers.
          * Checker simulation semantics hasn?t been yet defined. This is
       crucial. When the clocking event is checked ? Active or Reactive
       region. If in the Active region we will be (always) unable to
       assign ended/triggered sequence methods to checker variables, and
       this is bad. If in the Reactive region ? needs to understand what
       happens with the checker instantiation from a program.
          * Checker argument sampling (related to the previous issue, and to
       the 1900 section proposal Erik sent out Monday): are the checker
     arguments sampled unconditionally unless they are automatic or const,
     or are they not sampled at the checker instantiation, but their
     sampling is defined inside the checker itself ? the values are
     sampled in concurrent assertions and in the RHS of the assignments,
     but not in deferred assertions and not in final procedures. If the
     actual arguments are constants, they are not sampled.
     * Random simulation of free variables. If not ready should we use
       keyword rand?
          * Covergroups in checkers 
   5. Other technical topics
          * Opens? 


====================Summary==============================
1.  Checker arguments
    a.  Will be sampled if checker appears in module/interface/program
    b.  Will not be sampled if checker appears inside another checker
        Will "inherit" the sampled/not-sampled/const cast status from
   enclosing checker.
2.  We won't put a restriction on assertions items in procedural code
    inside checkers.
3.  Checker simulation semantics
    a.  Procedural blocks will execute in Reactive region within checkers
        This allows the use of triggered sequence method in assignments.
    b.  NBA assignments will be updated in Re-NBA region
4.  Random/free variable solving
    a.  Constraint solver will solve for free variable values before
   observed region.
    b.  Free variables will not be sampled when they appear in procedures
   or assertions.
====================Notes==============================

1.  Patent Policy:
    Move:  Gordon  Consider the patent policy read
    Second:  Steve
    Approved unanimously
    Ref:  http://standards.ieee.org/board/pat/pat-slideset.ppt


2.  Approve minutes.
    Move:  Dmitry:  Approve the minutes from the last meeting.
    second:  Gord:
    Approved unanimously

3.  Action item Review

    * 2398: New semantics for concurrent asserts in procedural code (Erik, Gord)
    Erik   - Sent out a draft last week.
          - Should be ready to vote next week.

    * 2370: $past in Procedural code
    Jin      - Need a few days extension

    * 1900:  Checkers 
    Dmitry   - Initial draft for checkers definition
    Mike   - For free vars: Sent initial draft, has a new revision ready
    Tom      - Edits to part 1 of 1900 uploaded

    * 2182:  VPI Diagrams for checkers
    Erik   - Chuck Berking from CC will review the proposal

    * 1728:  Let statement
    Dmitry   - Ready to vote.
          - Wrote up separate proposal to allow inferred value functions
        in Let.  It is Mantis 2413.
          - Gord will Review
    Abby   - Let is covered in 1503.  Has same issues
          - But 1503 is approved.
    Dave   - If changes in LRM, need new Mantis item
    Lisa   - Don't think it was put in the LRM
    Dmitry   - Has taken out VPI
          - Has already created Mantis item 2414 for VPI issues
    * 1549   - Is in latest draft
          - Add a new Mantis item for this.
      - Gord will create it.

    * New "@edge clk" proposal
    Erik   - Will talk with Jin.


4.  Technical issues for checkers
    * Checker instantiation semantics:
    Dmitry   - Should be same as property instantiation
    Gord   - Yes.

    * Checker simulation semantics.

    Tom      - Use of triggered sequence method seems to be introducing
            too many complications.  Lots of special-case rules required.
      - Inputs sampled or not?  
    Erik   - What about const cast inputs to checker when instantiated
            in procedural context.
          - Are checker inputs sampled or not?
    Gord   - One reasonable definition
          - Checker instantiated in module/interface: inputs are sampled 
      - Checker within checker: inputs not sampled
    Dmitry   - What about property & sequence arguments to checkers?
      - Also, this means that disable signal will now be sampled.
      - But it should work.
    Erik   - One other question:  Should we disallow assertion items in
        procedural code inside checkers?
    Tom      - Should not be a problem to disallow
    Dmitry   - OK, but still want to allow in initial blocks
    Gord   - Not sure how this simplifies things.
    Erik   - Think about checker instantiated in procedural loop.   Inside
        the checker is an assertion inside an always block.  How many
        executions of the checker will occur?  Will it be controlled
        by always procedure in checker?  or by the loop that the
        checker is instantiated in?
    Gord   - See it as controlled by always procedure in the checker.
    Erik   - So in this checker, an assertion placed within the checker,
            but outside any procedure, would be controlled by the loop
        that the checker is instantiated in.  Any assertion inside
        a procedure within the checker, would be controlled by that
        procedure.
    Gord   - One interesting case:  If enclosing procedural loop never 
        executed, the assertion inside the procedure in the checker
        will still be executed.

    Steven   - Is this well defined?
    Gord   - Const cast, explicit or implicit on the instantiation will
        determine the usage.
      - If actual argument contains const cast, and the formal
        argument is used inside the checker in a procedural context,
        that is an error.


    Erik   - So what about timing of always blocks
    Dmitry   - Need to execute in reactive region
    Tom      - If inputs to checkers are always sampled, then this should be
            OK.


    * Random simulation of free variables
    Mike   - Wrote up rules about solving in preponed.
          - Open Issues
      - Mirek not happy that it is optional to find a solution
    Gord   - This has got to remain like this
    Mike   - assume property does two things:
          - In preponed, you solve,
      - in observed, you check  (you'll find out that you didn't get
        a solution)
    Erik   - Does solution consider all assumptions
    Mike   - Everything other than free vars is state, which is read.
          - Free vars are static too?  Could assumptions refer to
        const cast?  HOw could this be solved?
    Gord   - Concern: you have a varying constraint set.
    Mike   - Definitely a performance problem . . .
    Erik   - Assumes involving const cast formals don't participate in the
            solution
    Erik   - What set of assumptions is used
          - If random variable passed to sub-checker, would assumptions
        inside sub-checker be considered?
    Gord   - Problem is defining what set of assertions should be considered
          - It's a quality of results problem

    Mike   - Mirek had concern:  Does solving in pre-poned introduce race
            conditions?
      - Also you have to know that a clock is going to occur in the
        timestep.

    Gord   - Yes, that's a problem
    Mike   - Change to say that solution occurs before observed.
          - free variables will not be sampled.


    * Mantis 2415:  Dmitry's proposal re: triggered and ended
    Lisa   - Will review
    Tom      - Will review

    * Covergroups in checkers:
    Tom      - Will modify covergroup proposal



Next meeting:  7/1

-- ErikSeligman - 29 Jun 2008