sv-sc Meeting Notice, The next meeting of the sv-sc will be held on Monday April 21, 9am-11am (PDT). Toll Free Dial In Number: (866)839-8145 Int'l Access/Caller Paid Dial In Number: (215)446-3660 <--- new number! ACCESS CODE: 9301228 Agenda: 1. Review the patent policy 2. Approve the minutes from the April 7, 2008 meeting Attached are the minutes from the first meeting. 3. Election of committee chair We have a nominee (thank you Erik) 4. Review of action items 5. List of Mantis items to be addressed 1. 1900 - checkers 2. 2088 - allow covergroup in checkers 3. 2089 - allow final block in checkers 4. 2110 - Allow checkers in procedural for loops 5. 2182 - Elaborate VPI diagrams for checkers 6. 1995 - Allow concurrent assertions in for loops 7. 1728 - let statement 6. Next meetings Possible f2f meeting May 5, 2008 9am-11am - next conference call Note: This is the last notice that will go out to all of the other committees. We now have an email alias for the new P1800 sub-committee on checkers. At the first meeting we decided to refer to it as the "special committee". The new alias is sv-sc@eda.org If you would like to become a member of this alias, send an email to majordomo@eda.org With the following message body subscribe sv-sc your_email_address_here -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean. 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)Received on Sat Apr 19 12:30:46 2008
This archive was generated by hypermail 2.1.8 : Sat Apr 19 2008 - 12:34:19 PDT