Minutes SV-AC 08/04/03
Written by: Stephen Meier

SV-AC v3.1a Meetings:
	Every Monday 9AM
        Domestic: 888-635-9997
        International: 763-315-6815
        Participant: 959066#


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[xx] Faisal Haque (Cisco, Chairman)
v[xx] Steve Meier (Synopsys, Co-Chair)
v[--] Roy Armoni (Intel)
v[xx] Surrendra Dudani (Synopsys)
v[--] Cindy Eisner (IBM)
v[xx] John Havlicek (Motorola)
n[--] Richard Ho (0-in)
v[xx] Adam Krolnik (LSI)
v[xx] Joseph Lu (Sun)
v[-r] Erich Marschner (Cadence)
n[--] Andrew Seawright (0-in)
v[xx] Bassam Tabbara (Novas)
v[--] Tej Singh (Mentor)
n[x-] Connie O'dell (Consultant)
n[x-] Hillel Miller (Motorola)
	
==+------------------------- 07/27/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. Operating Guidelines

Vote on operating guidelines.  All in agreement with guidelines as sent to SVAC titled Operating_Guidelines_SVAC.pdf

2. Enhancement List

We walked through Rev1.3 of SVv3.1a enhancement list.

PSL features required:
	Faisal posed question to John on his view with respect to enhancements from PSL that are important requirements to SVA.  John indicated that he is hesitant to add all the formula operators from PSL.  He feels that enhancements in nesting of properties are important, but he feels the rest of the language is powerful enough.

item 1 assume:  was generalized to review and proposed enhancement considering all PSL directives.  There may be need for restrict directive to drive formal tools.

item 5 clock_var_assign:  Adam asked why the enhancement could not just use variable assignment from always @ with non blocking assignment.  Surrendra indicated that $past, ended features are not available on verilog nba.  The proposal should review feasibility of extending nba's in contrast to adding a new form of sampled assignment.

item 6: Adam clarified that requirement is to be able to use assertion values in messages, so when an assertion fails the related variables and status can be displayed in a message.

item 8 seq_param_module:  It was clarified that what is desired is an additional type which can be included on module port list.  This would be preferred to parameter.

item 9 inf_pass_arg:  Adam suggested that an alternate syntax for infinity be included which can be used everwhere (in ranges) and that way users could have one consistent syntax.

item 10: There was discussion on which form of implication would be extended.  It was indicated that both SVA forms would be supported.  John indicated that there would be similar restrictions for multi-clock to only support the non-overlapping form whenever clock changes between implication operator.  It was agreed to combine item 10 & 11 into single combined implication enhancement.

There was discussion on abort and if it should be supported within nesting and it was felt that it was good if it can be defined.

There was discussion on mapping to PSL.  John felt that there was good match with formula implication, but that the SERE implication was restricted to not allow nesting.

More general discussion on SVA mapping to PSL.  John feels that SVA maps fairly well into PSL with exception on a) local variables b) first_match.

item 12: temp_operators
	
	Hillel expressed requirement for dynamic recursive properties which get expanded at runtime based on content of data.  This feature is in CBV and has been useful.  The example given was on burst sequence length.  That the length could be identified and then a set of assertions generated which is as long as length of burst.  Each assertion would be parameterized to evaluate data item based on its assigned item #.  John indicated that this enhancement was discussed within FVTC and the challenge was in determining if the unrolling completes "ties off" and having a means to describe this restriction in LRM.

item 13: formal features

	There was no discussion of formal features.  Adam asked if more of PSL could simply be ignored.  He would like to write one set of assertions which could be used in both SV and PSL.  Steve indicated that any extension to SV syntax/grammer should be designed and accompanies by semantics description.  John indicated that any extension of SV to add more PSL features should take care to ensure clean support of local variables.  PSL does not have local variable support defined for the temporal operators.

3. Additional enhancements.

We reviewed Adam's email with enhancement suggestions.

1) it was discussed that a global clock could be created in $root and also that interfaces follow existing default clock and clock definition feature and in the limit a clock can be included within an interface.  Adam was ok with this clarification.

2) mod_port: Adam would like to ensure that error reporting gives context of the included block in terms of instance name (hierarchy reference).  He suggested that assertions be included within the mod_port.  Steve will discuss with BC leaders to review this request.

3) directives: covered under enhancement item #1

4) assertion in functions:  Adam wants to put assertions in functions as he wants the assertion to be with the design code.  Steve indicated the added complexity of functions in procedural context and needed to extract context.  Will add to enhancement list.

5) module argument passing: covered under item 8

6) PSL enhancements:  covered under items 12, 13

7) Using $past with gated clock.  Adam would like to have ability to model gated clocks in assertions.  Will be added to enhancement list.

Steve indicated he would update the enhancement tracking list and solicit comittments for making proposals.  COmittment is due by end of this week, proposals need to be in by September 15th.

Meeting Concluded