-- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean. Champions March 13, 2008 Conference call Thursday 8-10AM PDT Attendees: ---------- 1. * Stu Sutherland 2. * Surrendra Dudani 3. * Brad Pierce 4. * Francoise Martinolle 5. * Shalom Bresticker 6. * John Havlicek 7. * Dave Rich 8. * Neil Korpusik 1. Review IEEE patent policy http://standards.ieee.org/board/pat/pat-slideset.ppt Move: Brad - assume that the patent policy was read Second: Shalom Passed unanimously 2. List of Mantis items that are ready for review: ----------------------------------------------- 2.1 2219 SV-BC not clear whether continuous assignment of event is allowed - fixed - On February 18, 2008 the SV-BC unanimously approved this proposal via e-mail ballot. Brad - this is just a clarification Dave - events are now just like other variables Move: Brad - approve the proposal for Mantis item 2219 Second: John Passed unanimously 2.2 2173 SV-AC Add case construct for properties. - fixed - 2008-02-26: Voice vote to approve proposal and friendly amendments, 7y/1n/0a. MK voted no: The reason is that I do not think it adds any critical functionality. The friendly amendments were implemented in 2173_prop_case_080226_yf.pdf. - Shalom 03/10/08 I don't think the BNF footnote is needed. Regular cases have the same restriction with such a BNF footnote. - John flagged some places with missing ; in the proposal. 03/12/08 He flagged additional issues on 03/13/08 (shown below) There are some semicolon problems that need to be fixed. 1. When property_spec is used in a concurrent assertion statement, no semicolon is required. This needs to be preserved for backward compatibility. Under this proposal, a semicolon is required for the property_statement form "property_expr ;". 2. In a property declaration, there is an explicit ";" after the property_spec. This proposal will result in two semicolons when the property_statement has the form "property_expr ;". A possible solution is to have both property_spec and property_statement_spec, where the former is unchanged, i.e. property_spec ::= [clocking_event] [disable iff (expression_or_dist)] property_expr and the latter requires a property_statement in place of the property_expr. Then use property_spec in the assertion statements (unchanged) and use property_statement_spec in the property declaration, getting rid of the explicit semicolon there. . In the discussion of non-vacuous evaluation, the definition for vacuous vs. non-vacuous of case without default needs to be tight. This can be done as follows: CHANGE An evaluation attempt of a property of the form case (expression_or_dist) expression_or_dist1: property_stmt1 expression_or_dist2: property_stmt2 default: property_stmt3 endcase is non-vacuous iff either (expression_or_dist === expression_or_dist1) and the underlying evaluation attempt of property_stmt1 is non-vacuous, or (expression_or_dist !== expression_or_dist1 && expression_or_dist === expression_or_dist2) and the underlying evaluation attempt of property_stmt2 is non-vacuous, or (expression_or_dist !== expression_or_dist1 && expression_or_dist !== expression_or_dist2) and the underlying evaluation of property_stmt3 is non-vacuous. TO An evaluation attempt of a property of the form case (expression_or_dist) expression_or_dist_1: property_stmt_1 ... expression_or_dist_n: property_stmt_n [default: property_stmt_d] endcase is non-vacuous iff either (expression_or_dist === expression_or_dist_1) and the underlying evaluation attempt of property_stmt_1 is non-vacuous, or (expression_or_dist !== expression_or_dist1 && expression_or_dist === expression_or_dist_2) and the underlying evaluation attempt of property_stmt_2 is non-vacuous, or ... , or the default is present and (expression_or_dist !== expression_or_dist_1 && expression_or_dist !== expression_or_dist_2 && ... && expression_or_dist !== expression_or_dist_n) and the underlying evaluation of property_stmt_d is non-vacuous. By doing this, the statement about a case without default being vacuous "if (but not only if)" follows from this definition rather than being an independent and incomplete definition. You might want to start that sentence with "Therefore". By the way, I think that setting the case off with code formatting as I show above is much better than streaming it in the paragraph. . I recommend changing The set of semantic leading clocks of case (b) b_1:q_1 ... b_n:q_n default: q_d endcase is {inherited}. to The set of semantic leading clocks of case (b) b_1:q_1 ... b_n:q_n [default: q_d] endcase is {inherited}. In other words, show the default as optional so that the definition is complete. Shalom - Should it be sent back? John - thinks his issues need to be addressed. - the ';' issue is a backward compatibility issue. Stu - The proposal was updated today (john added it -- not approved yet). John - the new proposal has the changes that he thinks are needed. Brad - agrees with the ; issue John - The next change - the vacuous case was not completely specified. not in today's updated proposal. Brad - possibly create a new mantis for these changes? John - expects reasonable people will interpret it correctly, others may not. Shalom - another minor comment - was fixed in the new proposal. - case statement in properties (was added) footnote to bnf. Only 1 default clause allowed. Don't need that footnote. Not in the new version. FM - did the svcc look at it? - the svcc looked at Mantis 1900 yesterday. John - it is on the list for the svcc. Neil - It can't go to working group until the svcc reviews it. John - maybe put the vpi portions into a separate proposal. AI/Neil - bring up with the wg. Split into two pieces? don't hold up due to cc. Stu - what about unique and priority case? - assumes it isn't allowed. John - svac didn't have time to add in all the flavors of case Shalom - casex and casez also not included. John - they would require more considerations Brad - doesn't think all are necessary. Shalom - randsequence - it also has case (only one version) Stu - iff is used in the text. iff is not defined anywhere. Neil - a general issue, not a particular issue with this proposal. Shalom - will the IEEE complain? Stu - if they see it, they will. Shalom - only in clause 16? -- add to front of clause 16. John - used a lot in mathematical English. - could change all to "if and only if". - could add to friendly amendments. Shalom - already in the text of the lrm 16.4.7 Brad - editorial issue. Shalom - conditional on 1932 (LTL operators) John - 1932 rearranges structure of ltl? - this proposal is based on that change. - this proposal can only be done on top of 1932. Shalom - the contingency must hold. *** This proposal is contingent on 1932. a. ; - now in the latest proposal b. footnote - now in the latest proposal c. non-vacuous text - page 5 of proposal - reformating required Brad - New proposal - treat as a friendly amendment. Brad - other stuff - just vacuity - create new mantis - also the default part is optional Move: Brad - approve the proposal for Mantis item 2173, approve the new uploaded proposal, and create a new Mantis item for the other stuff. Second: John Oppose: Stu - John's issues should be done first. Passed with one opposed. AI/Neil - create a new Mantis item for the issue with vacuity and the default. 2.3 2106 SV-BC Clarifications needed for declaration before use of objects and type - fixed - Champions feedback for this Mantis item was placed into Mantis item 2304. This was agreed to in the Champions conference call of February 25, 2008. The Champions however neglected to vote on the proposal for 2106. Mantis item 2106 will have to go back to the Champions for a vote. - John flagged an issue with the note: The note at the end of the 6.18 changes has normative statements. Dave - Only that one sentence is a note, not the whole paragraph. John - we may need a paragraph break here. Shalom - if the note wasn't there, would it be clear? Dave - that is why the note is there. Sahlom - a forward typedef to a struct is possible. - Nothing in the LRM leads to the conclusion stated in the note. Neil - the note only discusses the cross-coupled case. - There are no handles to structures. Brad - struct is not an abstract data type. Dave - cross-coupling only applies to handles. Shalom - don't even need this note if no one will even think of doing it. Dave - people have tried to do this. - they have tried to create a circular reference AI/Neil - Create a new mantis on this issue. Shalom thinks it should be normative. Move: Dave - approve the proposal for Mantis item 2106 Note to editor - paragraph break (already there - stu) Second: Brad Passed unanimously 2.4 2100 SV-AC Add synchronous resets syntax as oppose to the asynchronous nature of accept_on/reject_on - fixed - 2008-02-21: Voice vote to approve, 7y/0n/0a. - Shalom 03/10/08 (2 minor typos) "except for it evaluates" -> "except that it evaluates" "troughout" -> "throughout" FM - any new keywords being added? John - just new operators. Brad - this same functionality can be achieved already. John - doesn't know how to do it in the general case. Shalom - bottom of page 5, typo if_a_becomes - no underscores required. - this proposal is being laid over the changes from 1757. - This sentence looks ok in 1757. Move: Brad - approve the proposal for Mantis item 2100 with Shalom's friendly amendment (3 minor typos) Second: John Passed unanimously 2.5 2097 SV-BC release/deassign with variables driven by continuous assignments - fixed - The proposal was sent back to the SV-BC by the Champions in the January 17th, 2008 conference call. The latest Email thread concerning Mantis item 2235 needs to be addressed. - On February 18, 2008 the SV-BC unanimously approved the attached proposal Shalom - the svbc said 2235 is a separate issue. Move: Dave - approve the proposal for Mantis item 2097 Second: Brad Passed unanimously 2.6 2069 SV-AC Formal semantics for coverage is missing - fixed - 2008-02-13: Passed by e-mail ballot, 6y/0n/3a. - John sent email 03/13 (right before our conference call) . p. 2, Change "satisfied on each set trace" to "satisfied on each trace". . p. 2, Change "satisfied on at least one set trace" to "satisfied on at least one trace". <part of the following suggested change> . p. 2. The phrases "trace that satisfies all the assumptions associated with the model" and "feasible trace" have not been defined that I can see. I guess that these are intended to mean the same thing. If so, I would change From: The following definitions describe assertion statement satisfaction on a set of traces: - assert property statement is satisfied on a set of traces if it is satisfied on each set trace that satisfies all the assumptions associated with the model. - assume property statement is satisfied on a set of traces if it is satisfied on each trace of the set. - cover property statement is satisfied on a set of traces if it is satisfied at least on one set trace satisfying all the assumptions associated with the model. An assertion statement holds globally if it is satisfied on the set of all feasible traces. To: (something like the following) Given a set of traces and a set of assumptions, the following definitions describe assertion statement satisfaction on the set of traces predicated on the set of assumptions: - A trace in the set of traces is _feasible_ if every assumption in the set of assumptions is satisfied on the trace. - An assert property statement is satisfied on the set of traces predicated on the set of assumptions if it is satisfied on each feasible trace. - A cover property statement is satisfied on a set of traces predicated on the set of assumptions if it is satisfied on at least one feasible trace. An assertion statement holds globally on the set of traces predicated on the set of assumptions if it is satisfied on every feasible trace. - From Lisa: Given that there now exists a "restrict" statement, and this is for formal, do we also need to make it clear that "assumptions" in this context refers to the set of properties defined by "assume property" and "restrict property" John - believes he knows what it means. The word feasible is used, but not defined. - Lisa has a fair question. Stu - "single trace" and "set of traces" is introduced as well. Shalom - trace is already used in lrm, but not defined in section 16. - mentioned in section 40, F Shalom - prefers changing trace to word. Move: John - For Mantis item 2069, ask svac to: a. address Lisa's question b. make John's changes. c. define "single trace" and "set of traces" or change "trace" to "word" Second: Stu Passed unanimously 2.7 2043 SV-BC $cast should appear in 19.5 Conversion functions - no change required - On February 18, 2008 the SV-BC unanimously approved Move: Shalom - approve the resolution of "no change required" for Mantis item 2043 Second: Stu Passed unanimously 2.8 2005 SV-AC Solution for glitch problem in immediate assertions - fixed - This Mantis item was in the feedback state during the review period for the Champions Feb 25, 2008 conference call. It will need to be reviewed for the next Champions meeting. - There was minor feedback from the cc Erik made an update to address this 03/10/08 - Erik made a few minor changes based on input from Shalom -- 03/10/08 "begin/end" should be "begin-end". "process'" should be "process's," I think. "different-process" should be "different process". - Erik - his latest was not posted - another version was sent out 03/13/08 "at yesterday's SV-CC meeting, they approved 2005, conditional on the Friendly amendment that the #define at the end (Annex N) be moved to after vpiIsClockInferred. So I made that change; the doc is attached. I guess we need to re-voice-vote this final amendment on Tues." Shalom - Erik updated it again with feedback from svcc. - not voted yet. Stu - that change just moved a line in a vpi diagram. Not a substantive problem. FM - question about "assert #0" doesn't behave like a normal #0. Stu - he also pondered this question. Not sure what else to do. Would probably require a new keyword. John - that was considered, but they prefered #0 Stu - it means move to the inactive region for rtl code. Brad - assume, cover, assert - all would need a new keyword? Stu - what about "restrict"? FM - concerned that users will assume #1 is also allowed. Stu - that is a good point. - he is ok with #0 here. Dave - thinks this is a good use of creative syntax. FM - it should be more like an nba. Sahlom - waits until end of active region - there is also a flush action which occurs. Surrendra - same as doing sample in the observed region. Shalom - no, not the same. Stu - similar to the unique case. - hopefully it won't be a performance issue for simulators, not using any actual regions. - would anyone ever want to see the intermediate values(using vpi)? Shalom - you would remove the #0 if want to see it... Dave - some debugging tools replicate the assertions. Stu - there is enough context here to recognize that it isn't a delay Dave - can this be in a function? ?? - yes. Shalom - page 5, 3rd paragraph from end, "Deferred assertion syntax is similar to simple immediate assertion syntax, with the difference being the specification of a #0 delay control after the keyword:" - "delay control" should be removed from this sentence. - indefinite article - before this can also be struct. Brad - it is a delay Dave - Not a "delay control" FM - still doesn't like the #0 Dave - We also use #0 in clocking blocks, for clocking block drive. Updating a register that will be driven in the future. - variable on the LHS is treated like something different from a variable. Dave - could possibly use an nba trigger here. ->> Shalom - likes #0 better, it is more intuitive Stu - agrees with Shalom Dave - #0 in a function, might be confusing to implementors. Move: Brad - approve the proposal for Mantis item 2005 Friendly amendment - strike "delay control" (p.5) Second: Shalom Abstain: FM - doesn't like #0, conveys a meaning that is not correct. Passed with one abstain. 2.9 1982 SV-AC 16.7: Description of actual arguments is unclear and maybe also inconsistent with other description of $ - duplicate - 2008-02-19 6y/0n/0a. John - resolved in another proposal (1549) - 1549 also had other stuff. Shalom - 1549 is in the approved state. Move: Brad - approve the resolution of duplicate for Mantis item 1982 Second: John Passed unanimously 2.10 1932 SV-AC Introduce LTL and other temporal operators - fixed - Failed Champions email vote of Feb 23, 2008. There were 2 no votes (Stu, John) Stu I vote no because this change potentially impacts many aspects of the standard. For example, the proposal adds a large number of new operators and keywords that have not been reviewed an accepted by other committees. Other committees need several weeks to consider this mantis item. This change is much too large to be introduced this late in the standardization process for a proposed 2008 standard. John - he sent a lot of input to the svac. m022508.txt - It appears that the changes have been made and it is ready for another review by the champions. - 2008-02-26: Voice vote to approve LTL.1932.080224.pdf and LTL_Formal.080225.pdf, 9y/0n/0a. Brad - are we still seeing debate in svac? - next - one of the new keywords Dave - thinks they should use other techniques and not add keywords. John - methods didn't seem to work out. Operators give a formula-like syntax. - LTL has existed for years. Dave - eventually and eventually_s is one possible approach Brad - eventually! (can this be used?) Dave - that would cause conflicts with existing parsing rules. ---> John - ac look at strong weak using methods. Stu - that would cut the number of keywords in this proposal in half. Shalom - a new language - long list of keywords. Dave - no longer a language - a list of commands. - looses something - takes away from conceptual view. now need to learn all these keywords. John - Motorola in 2002 - keyword issue back then they lost the argument. Shalom - Dmitry at f2f - one of first slides, using symbols. "What does it mean?" Looks like gibberish. That is the advantage of using words - more intuitive to follow. Fewer mistakes. Brad - that would be too low-level (no functions) John - there is a community of users that are familiar with these operators. Stu - likes descriptive - keywords in a very narrow context. Burns that keyword for all users. next, until John - nexttime - is a valid choice. Dave - strong eventually - why not have this? John - he suggested it, others said it was too long. Brad - would prefer _s at the end, There seem to be lots of divergent ideas here. Stu - likes Dave's idea of strong... John - Could have an operator that applies to a whold property, could call it strong or weak. Need to treat negation properly in that framework. If code with strong, could replace all strongs in a sub-property with a single word. Give up compatible approach for now, and understand that this will be augmented later. Dave - It should be implemented before being proposed. John - a donation will have the same issues. Shalom - SystemVerilog is already based on stuff from other languages. It looks like a patchwork. Dave - The svac is defining language features by committee. Stu - this one comes from psl. John - svac - is willing to make changes. - "If we ask for a rock we may just get another rock from them." Stu - would like to hear from other vendors about keyword clashes in legacy code. Ai/Neil - Working Group - keyword issue. How figure out how to proceed? Move: Stu - Send Mantis item 1932 back to sv-ac to resolve keyword issue and possibly reduce the number of keywords being added, also try to make them less common. Inconsistent use of strong - sometimes _s and other times strong. Second: dave Passed unanimously 2.11 For those Mantis items on the agenda that are listed as being duplicates 1852 SV-AC Ballot Feedback Issue STU2: Declarations on Assertions 1849 SV-AC Update VPI object diagrams for immediate assume, cover 1833 SV-AC JEITA: 16.3 Precise definition of immediate assertion 1786 SV-AC Definition of "if else" in Annex F seems broken 1564 SV-BC 4.16, glossary: inconsistent definitions of bit-stream type 0588 SV-CC 31.9 uses the term "user", and has grammatically incorrect 0587 SV-CC 31.8.7 Please replace the term "user" with a more accurate term Move: brad - accept resolution of duplicate Second: Dave Passed unanimously 3. Next meeting March 20 - Thursday 7:30-9:00am PDT -- March 13th continuation meeting March 27 - Thursday Working Group meetingReceived on Mon Mar 17 10:53:10 2008
This archive was generated by hypermail 2.1.8 : Mon Mar 17 2008 - 10:53:13 PDT