Minutes of the sv-sc sub-committee meeting

0 Day
7
0 Month
4
0 Year
8

a   Arturo Salz          - Synopsys
a   Bassam Tabbara       - Synopsys
a   Brad Pierce          - Synopsys
a   Cliff Cummings       - Sunburst Design
a   Dave Rich            - Mentor Graphics
a   Dmitry Korchemny     - Intel
a   Eduard Cerny         - Synopsys
a   Erik Seligman        - Intel
a   Francoise Martinolle - Cadence
a   Gordon Vreugdenhil   - Mentor Graphics
a   John Havlicek        - Freescale
a   Jonathan Bromley     - Doulas
a   Karen Pieper         - Accellera
a   Lisa Piper           - Cadence
a   Manisha Kulshrestha  - Mentor Graphics
a   Mark Hartoog         - Synopsys
a   Mehdi Mohtashemi     - Synopsys
a   Mirek Forczek        - Aldec
a   Neil Korpusik        - Sun Microsystems 
a   Shalom Bresticker    - Intel
a   Steven Sharp         - Cadence
a   Stu Sutherland       - Sutherland HDL
a   Surrendra Dudani     - Synopsys
a   Tom Thatcher         - Sun Microsystems


 **  Minutes taken by Neil Korpusik 
//////////////////  April 7, 2008 /////////////////////////

Agenda:
-------
1. Review IEEE patent policy
   -------------------------
    ref:  http://standards.ieee.org/board/pat/pat-slideset.ppt

       Move: Cliff - assume that the patent policy has been read
     Second: Mark
     Passed unanimously


2. Policies and guidelines
   
   - The sv-sc will follow the same Guidelines as the other Technical Committees.
     A copy of those Guidelines can be found at. 

   http://www.eda-stds.org/sv-bc/hm/5964.html

   - Meetings will initially be held bi-weekly
     The frequency will be adjusted as the need arises.
   - DAC (June) - some people will be busy.


      Move: Cliff - hold biweekly meetings on Monday's at 9am (PDT) 
    Second: Francoise
    Passed unanimously


3. Election of Chair/Co-chair

   Shalom  - doesn't understand the issues enough to be the chair.
   Several - wanted to retain voting rights and be able to take a position on
        any issues that arise.


      Move: Dmitry - Nominated Erik Seligman (Intel) as co-chair
    Second: Bassam
    Passed unanimously

   No one stepped up to take on the Chair position at this point in time. 
   Neil continued to Chair this meeting while we search for an official Chair.

AI/All - come to the next meeting with nominees for the Chair position.


4. Discussion

      Move: Stu - this committee should be referred to as 
        the "Special Committee"  (sv-sc)
    Second: Cliff 
    Passed unanimously


AI/Neil - we need an email alias for this group


   Neil - At the March 27th P1800 Working Group meeting it was agreed to form
     a new sub-committee to address issues related to "Checkers".
        - The committee will cease to exist after its work is completed.
   - The committee has until the end of July to complete its work.

   Below is the original list of Mantis items to be addressed by this committee. 
   The Committee can address other Mantis items as needed.

   1.  1900 
   2.  2088 
   3.  2089 
   4.  2100 - Shalom suspects this should not be on the list
   5.  2110 
   6.  2182
   7.  1995 - already approved - Erik is asking why on our list?
   8.  1728 - let statement - (agreed to in the WG conference call)

   I think we should add to the list for this new committee (Erik email)
   9.  2173 
   10. 2326
   11. 2327 


   Tom   - 1995 - Dave wanted it on the list 
  Steven - it deals with procedural code 
   Gord  - it isn't our intent to "tear up the tracks" on assertions in 
      procedural code
    - ok to reopen questions related to 2005. 
    Gord - we need to figure out the shape of issues and our direction. 
   Cliff - let's move through the list 
  Shalom - 2100 - adds a synchronous reset syntax 
    - assertions have a disable feature
      sometimes we want a synchronous version. (added by 2100)
    John - disable if 
      executes during timesteps in which the clocking event doesn't occur
      People agreed with this. 
         - sync_accept_on and sync_reject_on are being added.
      nestable operators, a sub-property can be made to apply to it 
         - adds synchronous version of accept_on and reject_on - only checked
      when the clocking event of the assertion is observed.
  Steven - sounds like 2100 is not related to the other issues
   

      Move: Cliff - Mantis 2100 be removed from consideration in this committee
    Second: John 
    Passed unanimously


    Erik - these 3 were suggested to be added by the svcc (2173, 2326, 2327)
    John - already have "else if"
    - There isn't much being added above and beyond: if else
    Erik - cc thought it looked complicated and punted on it
  Steven - cc should still look at it. 
    - bc should take a look?
  Gord   - derived operator?
    - not sure it is similar to typing of case
  Dmitry - these are not major proposals - vpi-related - why send to svbc?
Jonathan - hidden inside a property 


      Move: Cliff - recommend to have the Champions send 2173, 2327 to the 
          sv-bc (continuity with the LRM), 2326  to the sv-cc
          and not work on them in this committee 
    Second: Steven
    Passed unanimously
       

    Dave - suggested that we work on Mantis 1900 first (checkers)
  Dmitry - we could consider 1728 in parallel with 1900
         - 1900 incorporates 1728
    Dave - 1900 is at the core of the problems
    FM   - review assignments in procedural code first?
    Erik - that might be best to do first
    FM   - why want to put concurrent assertions in procedural code?
  Steven - sent out a list of issues - hasn't yet gone through Dmitry's response
    Gord - there are other issues that he also raised. 
      naming issues, assignments, what can do in other parts of the LRM 
         - name resolution issues in sequential contexts
         - consistently struggling with - in several of these proposals
      there seem to be synthesis assumptions and how they relate to 
      simulation semantics in various situations - the proposals are making 
      something illegal in order to address it.
         - We need a high-level discussion of assertions.
      How do assertions fit into a language which is defined in terms of 
      simulation semantics?
      How much irregularity are we prepared to deal with in the LRM? 
      Not sure how to deal with this. 
Jonathan - is the underlying assumption correct?
    - There will be some stuff that can't be simulated(e.g. strong operator)
    - Just accept that the simulator may only be able to handle part of 
      the LRM. 
    Gord - that might be the right direction. It would be a big change.
    - we then need to be very careful of how to phrase behavior in the 
      LRM - when are we talking about simulation and when not? 
         - he in the past referred to the assertion sub-language 
      if go this route - need to be very careful about how to phrase things
         - he had been told assertions are a first class participant. 
         - does it make sense to have a single LRM?
    - perhaps have a separate LRM for the formal aspects
      simulation, formal and synthesis
  Steven - may need to define both semantics for simulation and formal
    Gord - let is already falling in this category. 
  Steven - semantics of lrm are the rules of how to execute the lrm (simulation)
     - assertions seem to be defined in terms of formal.
    - free variables - defined as a formal capability - what to do for sim?
      random variables defined under a constraint. 
       formal - allowed to take on all possible values. 
      Why are free variables being introduced at all? 
      why not create an extension of constrained variables?
    Gord - 2 sets of semantics here
Jonathan - symbolic simulators - are well known
   Dave  - free vars are multiple states. 
    - there is a lack of understanding of what is already in the 
      constrained random area
Jonathan - it is an extremely sound idea to talk about free var as a symbolic 
      variables. simulators could then use one thread of simulation.
  Steven - formal would take all possible values into account. 
    - why not define in terms of simulation and derive formal from that?
  Dmitry - thought that there would be failures if use constrained random
  John   - infinite many and finite traces. 
  Steven - clearly there are other lrm areas that are abstracted for formal
    - no problem adding text for formal
    - strong operators - possibly no additional meaning for simulation
   Gord  - always_ff - simulation semantics (for sensitivity list) 
    - exist as hints and implied assertions for other tools - eg expected 
      to behave as a latch
         - so there are other areas like this - the LRM however defines the 
      simulation aspects, not what other tools do. 
         - name resolution, assignment semantics 
      where in a simulation cycle, etc.
    - some of that is immaterial for formal
    - stratified event queue doesn't apply to formal
      for simulation we need to know precisely where things occur
         - need to know constructs syntactically 
      need to have simulation semantics 
  Steven - might reduce to an existing construct - just need to use it this way.
    - not sure if this will happen - doesn't know enough about free vars
  Dmitry - there are important differences
   Gord  - if those are only in formal domain 
    - rand in a checker - may be equivalent to free var for 
      simulation semantics
  Steven - might require some additional annotation just for formal
  Dmitry - if start with simulation semantics - free vars might be similar to 
      rand
    - for formal - it is just one possibility to replace with rand 
      assert violation - witness for cover properties - becomes the free 
      vars for the trace
      If say all simulators consider free vars as rand - some distribution. 
   Gord  - part of problem is - definition of what tools might be doing. 
      LRM - use base language to create a tool that does what they want.
          - synthesis, etc.
          - base language has always been defined in terms of simulation
         - we will run into lots of issues if define in terms of other tools. 
    - Would like to stick with what LRM has traditionally done. 
      For other tools - a tool issue not an lrm issue.
  Dmitry - not against rand vars 
    - formal semantics is important - it should be the same for all tools. 
Jonathan - formal semantics of assertions - simply can't be simulated in 
      their completeness.
  Gord   - if simulation semantics are invalid - lets be more consistent
    - if using some construct for targeting formal then you create 
      situations which are invalid or more restrictive with the rest of 
      the lrm and simulation.
Jonathan - formal - one state - next state - doesn't map to simulation 
      scheduling semantics
  Dave   - there is a question of how to represent it in the LRM. 
  Steven - if need to have formal definition - use an appendix
  Dave   - when these constructs are put in the LRM - it isn't clear what tool 
      needs to follow them.
  John   - checker proposal - thought there was some discussion about simulation 
           versus formal
    - there was some intent to do that
   Gord  - the interactions are important 
    - value at a time slice, semantics. 
      all part of the behavior in a simulation.
      some of this was not stated at all. 
      reading values, etc. 
    Tom  - random assignments - random stability, etc. - not defined 
   Gord  - debuggers - need to know when updates occur - tools will diverge
      if not well defined 
   Neil  - do we all agree that the simulation semantics need to be completely 
      defined?
      Sounds like we all agree - so we have some work to do.
    John - not all issues Gord raised have been defined.
    Gord - if have constructs that prevent regularizing our assumptions there 
           will be problems. 
         - related to composability of large designs.
    Mark - there are a lot of things added to the language which 
      make composability harder. 
      Parameterized classes - what does it mean for separate compilation? 
  Steven - similar to parameterized  modules 
    - we have managed to deal with that. 
   Gord  - bind - and when do types become known. 
      may be resolvable issues 
    - binding checkers - changes the entire semantics of bind to now
      working with module declaration contexts. 
         - doesn't want to restrict discussions to current set of proposals. 
      Some people have extensions in mind. Need to be aware of 
      future extensions. We could have a hole.
         - wants people to bring out future use-models.
    - only for things that people already have in mind. 
    - would be good to have this rumbling around in our heads 
      when we discuss this. 
   Dave  - free vars - might need to be independent of checkers. 
  Dmitry - clock based entities 
   John  - what would make it tough to use elsewhere?
  Dmitry - would need always @(posedge clock). 
  Steven - raising point that free vars are synchronous to a clock 
    - not consistent with other SystemVerilog variables
    - could possibly use them in a clocking block
   Gord  - if a synchronous issue, could possibly be other ways to do this.  
      possibly be reasonably broadened so they can be regularized for 
      simulation.
  Dmitry - it isn't straight-forward
  Steven - want to be wary of argument that since something will only be in a 
      checker as being the reason why there is no problem. 
         - because formal only looked at a clock edge. 
    - Could turn it around to be:
      simulation can look at it any time and then formal would only look 
      at clock edge.
   Neil  - how get to conceptual agreement?
   Gord  - ask svac - not just where are we now
    - what are the use-models
    - synthesis view
    - not opposed to all semantics in lrm - but needs to be consistent.
    - brain storming of how to use this stuff 
  Steven - there is a gap between the formal people and simulation people. 
  Gord   - short-term - will go back to his list of issues
    - doesn't want to focus on narrow issues too soon. 
Jonathan - Gord - pull together a summary of his set of concerns. 
    - having one doc for all his issues would be good. 
   Stu   - would like to see something from the formal people 
         freevar - why an existing SystemVerilog construct can't be used
         - has read all of 1900 and doesn't understand why existing constructs
      can't be used.
   John  - step back from current proposal
    - what were the essential capabilities addressed by the proposal. 
      choices from which a selection was made in the proposal. 
         - some people see issues with current proposals. 
      what are the capabilities being provided - what are the choices. 
         - Dmitry did do some presentations - exist in premables or 
      auxiliary presentations.
   Gord  - the presentation dealt with the rationale. 
      The alternatives and trade-offs were not in there. 
   John  - thinks he would not be able to write up the set of choices
    - The proposal authors would be the best to do this. 
   Dave  - we need to see the requirements of the feature not the proposal 
      itself. 


AI/Dmitry - possibly distill down to a set of requirements. 
AI/Dmitry - send out his slides
AI/All    - read 1900 - 2 part proposal
AI/Dmitry - list of reasons why existing constructs can't be used - why not 
       straight-forward.
AI/Gord   - put together his list of issues
AI/Steven - put together his list of issues with procedural code



5. Next Meeting 

   April 21, 2008   9am-11am (PDT)

-- ErikSeligman - 21 Apr 2008