Minutes of the sv-sc sub-committee meeting, May 6, 2008

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

    0220 Day
    6817
    0000 Month
    5444
    0000 Year
    8888

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

====================Agenda==============================
Agenda:

    1.  Review the patent policy
    2.  Approve the minutes from the April 28, 2008 meeting,
        available at 
http://www.eda.org/twiki/bin/view.cgi/P1800/SvScMeetingMinutes20080428
    3.  Logistics topics
           * Face-to-face reminder: Wed 5/14- Thurs 5/15 in Bay area.
       Wed. meeting will be at Mentor, Thurs at Sun.
       Need to clarify addresses & meeting times.
           * Next week's regular meeting (Tues 5/13): confirm that it's
       still happening, or decide to cancel.
    4. Technical topics
           * Concurrent assertions in procedural code:
       continue discussion of last week's proposal, summarized at
    
http://www.eda.org/twiki/bin/view.cgi/P1800/ConcurrentAssertNewProposal.
       o Have we come up with complications since last week, or do we
         want to continue down this path?
       o Are we ready to move forward / formalize, or should we back off
         to the 2005 standard in order to continue?
       o Should we combine with shadow variables as discussed at bottom of
    
http://www.eda-stds.org/sv-sc/hm/att-0049/EmbeddedConcurrentAssertions__080422dk.pdf? 

           * Checkers as variant modules, and argument-passing concerns:
       report-out on John/Gord discussion (last week's action item), and
       identify issues needing resolution.

====================Notes==============================

1.  Patent Policy:  Neil:  Patent policy was updated on March 25, 2008
     Erik reviewed the new patent policy.
     ref:  http://standards.ieee.org/board/pat/pat-slideset.ppt


2.  Approve the minutes from the April 28, 2008 meeting
 
http://www.eda.org/twiki/bin/view.cgi/P1800/SystemVerilogSpecialCommittee

     Move:  Gord - approve the minutes from April 28.
     second:   Lisa
     Passed unanimously.

3.  Face-to-face meeting scheduled Wed 5/14, Thu 5/15
     5/14 at Mentor starting at 9:30am PDT
     5/15 at Sun    starting at 7:00am PDT
   NOTE:  Sun requires pre-registration of visitors.
      Sun does have a wireless network with guest access

     AI/Neil - Send address information to Erik.
     AI/Erik - list of attendees to be pre-registered.

     Should  regular phone conference be cancelled.
        Yes.

4.  Technical Topics

a.  Concurrent assertions in procedural code

     Erik    - what is Dmitry's feedback on the idea of triggering 
concurrent
         assertions in procedural code?
     Dmitry  - For concurrent assertions in combinational  code - need 
to avoid
         glitches
       - Assertions need to be clocked with a system clock
       - If they are not clocked with a clock, triggered using an if
         instead - it will not serve the user properly.

     Gord    - Didn't follow the argument

     Stephen - Thought that assertions could not appear in combinational 
processes.
     Tom     - Assertions may appear in always_comb:  There is a requirement
         that assertions have a clock.  Clock must be explicit, or inferred
         from a default clocking. If a clock is inferable from
         context, there is a requirement that any explicit clock in the
         assertion matches the clock inferred from the process
     John    - There was a proposal to relax the restriction on matching 
clocks.
     Francois- Also thought that assertions were not allowd in always_comb
     Mike    - Is there a difference between sampling and launching?
            - The values will not be sampled at the same point that the
         assertion is launched
     Gord    - Proposal says that enable condition would essentially 
schedule
              the assertion for evaluation.  Would need to de-glitch somehow.
         Assertion still waits for clocking event.  The clocking event
         is what commits to evaluating the assertion.

     Erik    - Do we want to go down this path?  It's a big change from 
2005.
     Steven  - Solves his issues.
       - Aligns assertions w/ procedural code
       - Allows for assertions in procedural loops
       - Doesn't require unrolling of loops
       - Allows for assertions in tasks & functions

     Dmitry  - Doesn't understand how this would work
     Gord    - This is different from a re-write.  It's not inlining and
         unrolling?
     Dmitry  - How can we describe this in formal semantics?

     Steven  - Example:  Assertion in a loop w/o static bound
              e.g.  for (i=0; i<foo; i++)  // foo is a variable
       - Process:  Start executing loop
      Every time you reach assertion point:  you schedule assertion
      evaluation:  Loop index variable value at this point is passed
      to scheduled evaluation.  May require some syntax to identify
      variables which use current value at scheduling time (not from
      preponed region).
       - If there's a glitch and loop has to execute again.
          Repeat process:  remove previously scheduled evaluations from
      queue.
       - In observed region:  scheduled evaluations begin (assuming
      clocking event occurs this time step).

     Dmitry  - You have changed the clock for the assertion
     Steven  - Have not changed the clock.  The clock is what determines 
when
         evaluation begins.

     John    - Question:  What if dispatch occurs in a timestep with no 
clocking
              event?
     Gord    - If timestep you are in has a clocking event, execution 
occurs in
         observed region of same timestep
       - If procedural code is run in between two clock events, then it's
         enabled when next clocking event occurs.

     Mark    - How you you know which variables need to be sampled?
     Gord    - Already can't sample automatics
     Gord    - Current semantics say you have to sample everything
         Optimizations are possible:  Constant bounds loop would allow
         optimization to not sample variables if sampled values never used.
       - Need to keep distinction between semantics, and possible
         optimizations.

     John:   - We are not changing assertion semantics:  Only changing the
         simuation implementation.

     Mark    - What about function called from assertion:  Does it need to
         sample its arguments?
     John    - Already have this problem:  Function called from assertion is
         passed sampled values.
     Erik    - would like to see an example.
     Gord    - suggest that you go back and look at the definition of 
deferred
         assertions.
         "attempt"
             - the way that you decide to do an attempt is the same as a
         deferred assertion.
     John    - the annex doesn't say anything about loops or unrolling.
       - the formal semantics don't even say how to do the sampling.
     Dmitry  - We have the notion of flow.
       - If a loop is not unrollable - you are chaning the assertion flow.
     Gord    - Doesn't understand how he thinks we are changing the flow.
     Dmitry  - Don't  understand how non-unrollable loops could be described
         in semantics.
     JOhn    - Our formal semantics annex doesn't rely on simulation
         One way to describe:
      <dispatch_event> |-> @(<assertion_clk>) <assertion>
     Gord   - if no temporal logic, it could even be re-written as a
        deferred assertion.
     Erik   - willing to meet with Dmitry off-line.  (Dmitry agreed)

     Erik   - Let's put together presentation for face-to-face
   AI:  John will prepare a presentation on this
       Steven will help on simulation semantics.
       Gord will help too.
       Anyone else who has an example, should submit it to John.


Argument passing:
     Gord & John -  Have exchanged some e-mails.  Not really at a point 
where
   they have a complete understanding of all issues.

       Gord - we don't yet have everything in our heads well enough yet.
       Erik - What about checkers
       Gord - Checkers are a more general example
      - sequences and properties need to be dealt with first.
      - trying to get traction on args to sequences and properties first.
       Gord - taking as a starting point - need to be able to reason about
        an assertion, independent of the body of the assertion.
       Erik - would have to be faced in 2005 lrm
       Gord - yes, and it is a problem in the 2005 lrm.

   AI:  Gord to have something for f2f


Other Issues:

     Erik   - What were other issues with checker:
     Gord   - Checker variables,
        This is not as big an issue.
     Erik   - What are other major issues?
     Gord   - Semantics of Let:  Hierarchical issues w/ let.
        This is the bigger issue.
     Erik   - Why is it an issue:
     Gord   - Let has macro-like semantics.  Basically smart macros
        Typing & expression results not consistent w/ other kinds of hier
        references.  An XMR in a let is not consistent with other XMRs.
      - Other constructs have reference to a thing.  Type of a thing
        doesn't change.
      - Let:  general expression.  context type infor must be passed in to
        body before we can know its type.
      - An xmr normally has a target with a self-determined type.
        The self-determined type is not impacted by the reference
        Let changes this:  pretty scary.
     John   -  eg.  a + b:  could lose carry-out
     Gord   - If a, b, are 8-bits, self-determined type of a+b is 
8-bits.  In an
       expression a,b extended to 32-bits to do evaluation:  therefore,
       context-determined type is 32 bits
     Erik   - as a user, wants untyped arguments and thinks of 
optimization as a
        less important issue.
            - 1800-2005 already supports untyped.
     Gord   - and it is supported across all situations?
      - vendors will put in restrictions in order to implement efficiently.
      - large designs, composability, consistency across vendors will suffer.
            - with today's rules only a subset will be consistent.

     Mark   - Even if you had type parameters for sequence & properties, 
this
        would not solve the problem.
     Gord   - Typed formals would help
     Dmitry - I don't understand need to pre-compile sequence & property
        definitions.
     Gord   - Why can't prototype of sequence be sufficient to compile a 
block
        This is important for consistent behaviour across tools.


     Gord   - let is inconsistent w/ rest of the stanard.
     Dmitry - Important thing is to have a generic integral type.
       AI:  Dmitry will present his motivations at f2f

     Dmitry - as from lib:  People now use untyped arg.
        Need to put integral value, not prop or seq
        We currently don't have generic integral type.
     Gord   - What you need is an unconstrained bit-vector
        Would not have objection to that.
        2-value/4-value:  either way.
        This is a much simpler problem.

     Dmitry - Doesn't understand how this solves problems.
     Gord   - His concern Type propagation from inside sequence to 
outsie context
        e.g. passing a+b  Okay to pass as unconstrained bit vector.
        problem is where type of a+b is influenced by it context within
        the seq/prop

     Mark   - Issue  w/ let is that it has no type
     Gord   - Correct.
     Neil   - Sounds like people in AC just not aware of tough cases.

       AI:  Gord:  prepare a few slides on this issue.
       AI:  Dmitry:  put together something on let.  What are the use cases
          that are needed?

     Mike   - thinks that if we see the sv-ac use model we might be able to
        come up with something that is "less scary"
     Dave   - One example is unconstrained array from VHDL
     Mark   - Type calculus is complicated  very few users understand it.
   
     Gord   - We have users that question what we are doing in certain 
cases.
        They are surprised when they see how the reasoning confirms the
        tool behavior.
            - Testbench code - people with a c++ background are in shock 
over
        the testbench syntax.
        We should have had a bigger split from dut and tb.
     Mark   - let is a delayed macro
     Gord   - it interferes with separate compile and IP, etc, since you 
need to
        deal with it in a very late manner.
        Desire is to have precompiled and boxed up ip.
        If use let in there - dangerous to treat let as a macro in that IP.
     Mike   - can get a billion errors if have let in there. The IP 
auther can't
        make their code bullet-proof.
       Mark - You wouldn't use xmrs from IP if you want it to be 
bulletproof.

-- ErikSeligman - 09 May 2008