SvScMeetingMinutes20080506 < P1800

P1800 Web>SystemVerilogSpecialCommittee>SvScMeetingMinutes>SvScMeetingMinutes20080506 (2008-05-09, ErikSeligman) (raw view)EditAttach
<verbatim>
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.

</verbatim>


-- Main.ErikSeligman - 09 May 2008
Topic revision: r1 - 2008-05-09 - 19:17:17 - ErikSeligman
P1800