Minutes SV-AC 10/20/03 Written by: Surrendra Dudani SV-AC v3.1a Meetings: Next meeting October 27 9am PST code for the conference call: Domestic: 888-635-9997 International: 763-315-6815 Participant: 274372# Attendance Record Legend: x = attended - = missed r = represented . = not yet a member v = valid voter (3 out of last 4 or 75% overall) n = not valid voter v[xxxxx] Faisal Haque (Cisco, Chairman) v[-xxxx] Arif Samad (Synopsys - Co-chair) v[xxxx-] Roy Armoni (Intel) v[xxxxx] Surrendra Dudani (Synopsys) n[-----] Cindy Eisner (IBM) v[xxxxx] John Havlicek (Motorola) n[-----] Richard Ho (0-in) v[x-xxx] Adam Krolnik (LSI) v[xxxxx] Joseph Lu (Sun) n[--x--] Rishiyur Nikhil (Blue Spec) v[-x-x-] Koushik Roy (Cadence) n[-----] Andrew Seawright (0-in) n[xx---] Bassam Tabbara (Novas) n[-----] Tej Singh (Mentor) n[-x-x-] Connie O'dell (Consultant) v[-xxxx] Hillel Miller (Motorola) ==||||+-------------------------- 09/15/03 ==|||+--------------------------- 09/22/03 ==||+---------------------------- 09/29/03 ==|+----------------------------- 10/13/03 ==+------------------------------ 10/20/03 Historical Attendance from SV3.1 through 4/21/03 v[xxxxxxxxxxxxxxxxxxxx----x.] Faisal Haque (Cisco, Chairman) v[xxxxxxxxxxxxxxxxxxxx-x-x-x] Steve Meier (Synopsys, Co-Chair) v[xxxxxxx-xxxxxxxxxxx-xxx--x] Roy Armoni (Intel) v[xxrxxxxxrxxxxxxx-x-xxxrxx.] Surrendra Dudani (Synopsys) v[rxxxxxxxxxxxxxxxxxxxxxrxrx] Cindy Eisner (IBM) v[xxxxxxxxxxxxxxxxxrxx-xxx..] John Havlicek (Motorola) n[--xxx--xxrxxxxxx-xx-xxxxx.] Richard Ho (0-in) v[-xxxxxx-xxxx-xxxxxxxxxxrx-] Adam Krolnik (LSI) v[xxxxxxxxxxx-xxxxxxxxx---xx] Joseph Lu (Sun) v[rxxxrx--xxxxxxxxxxxx--xxxx] Erich Marschner (Cadence) v[-xxx-x-xxxrxxxx-x-xxxxxx-x] Andrew Seawright (0-in) v[x-xxxxxxxxxxxxxxxxx-xrxxxx] Bassam Tabbara (Novas) v[-xxxx-x-xxxxx.............] Tej Singh (Mentor) n[x-x--xx-xxxx..............] Connie O'dell (Consultant) n[---xx-x-xxx-x--xxx-x--xx-x] David Lacey (HP, OVL Chairman) n[-x--x-xxxxx---x...........] Hillel Miller (Motorola) n[-----xxxx.................] Kurt Shultz (Motorola) ==||||||||||||||||||||||||| ==||||||||||||||||||||||||+- 07/09/02 ==|||||||||||||||||||||||+-- 07/25/02 ==||||||||||||||||||||||+--- 08/01/02 ==|||||||||||||||||||||+---- 08/08/02 ==||||||||||||||||||||+----- 08/15/02 ==|||||||||||||||||||+------ 08/22/02 ==||||||||||||||||||+------- 09/05/02 ==|||||||||||||||||+-------- 09/12/02 ==||||||||||||||||+--------- 09/19/02 ==|||||||||||||||+---------- 09/26/02 ==||||||||||||||+----------- 10/03/02 ==|||||||||||||+------------ 10/31/02 ==||||||||||||+------------- 12/03/02 ==|||||||||||+-------------- 01/23/03 ==||||||||||+--------------- 01/30/03 ==|||||||||+---------------- 02/06/03 ==||||||||+----------------- 02/13/03 ==|||||||+------------------ 02/20/03 ==||||||+------------------- 02/25/03 ==|||||+-------------------- 03/06/03 ==||||+--------------------- 03/27/03 ==|||+---------------------- 04/03/03 ==||+----------------------- 04/08/03 ==|+------------------------ 04/10/03 ==+------------------------- 04/21/03 1) Action Items * John: break up his proposal to separate discussion of nested implications and boolean connectives.No need to provide detailed instructions for LRM changes * John: add the proposal for if-then-else construct in the boolean connectives proposal for properties * Faisal: Inform TCC that John's proposals will not contain LRM changes yet. Once approved, the LRM changes will be added and further proposed for approval 2) Minutes * Adam discussed his proposals for extension item 15 and 16. Surrendra: Importing assertions via modport belongs to SV-BC, as it requires passing a labelled statement. Suggested to refer to SV-BC committee. Faisal: Will defer to SV-BC committee. It will be a request to allow passing of labelled assert statements via modport. Adam: Suggested to combine items 15 and 16 * Adam discussed his proposals for extension item 13. Surrendra: Can the assertions in functions use variables passed in as arguments to the function? Adam: Yes. The variables will follow the boolean expression rules. Surrendra: will the context inference pass through the function? Adam: yes Surrendra: Is function then allowed only where context inference can be obtained for clocking Adam: Yes. That would be the case. * John summarized two conflicting requirements related to the issue of local variable printing for debugging 1) prinrtf type messages wherever needed in the assertion. This would require multiple points in the assertion for printing, and possibly negating the assertion for failure detection at the end 2) one common error message for all failure of the assertion. Here, the problem is how to know which local variables to print. Surrendra: 2) is useful for simple cases, but for more complex cases, its not clear Adam: Instead of solving big problems, can we not provide a solution for simple cases? John: Can you define a simple case? Surrendra: We would need other mechanisms to specify an error message for a property, and be able to disable it when not desired John: Would it require additional syntax? Surrendra: Yes. * John discussed dividing his property extension proposals. Suggested to not rewrite two proposals with explicit detailed instructions for LRM changes, as they are laborious and wasteful, if the proposals are not accepted. Surrendra: Should propose two-step process, where the propsals are reviewed and voted based on the concepts. If approved, then explicit LR changes could be proposed for voting. Faisal: Agreed. Will inform TCC as it requires a shift in th eguidelines for proposals. All proposals are expected to be in the form of LRM changes. * John discussed adding if-then-else and case constructs in the property layer, and possibly to sequential layer. This makes syntax more explicit about the intentions of the writer, as well as providing guidance for the semantic analysis for formal tools. Otherwise, one has to express properties in the form of disjunctions. Adam: I'm afraid of the complexity in the language. Faisal: How much more complex is it? Adam: I'm not necessarily opposed to the idea, but just a caution. John: I think at least if-then-else would be very useful. We can live without the case statement Adam: Why would you want if-then-else instead of "or". John: Because I'm more likely to do case splitting, than disjunction, at least at the property layer. Surrendra: if-then-else is already present in the constraint language. So, it makes sense to align the two features Faisal: Will discuss Surrendra's proposal's next week