Minutes SV-AC 09/22/03
Written by: Arif Samad

SV-AC v3.1a Meetings:
        Next meeting September 29
        Domestic: 888-635-9997
        International: 763-315-6815
        Participant: 959066#

Note: starting with the 10/6 meeting there will be a new
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[--xxx] Steve Meier
n[x-x--] Roy Armoni (Intel)
v[xxxxx] Surrendra Dudani (Synopsys)
n[-----] Cindy Eisner (IBM)
v[xxxxx] John Havlicek (Motorola)
n[-----] Richard Ho (0-in)
v[xxx-x] Adam Krolnik (LSI)
v[xx-xx] Joseph Lu (Sun)
v[x-rr-] Kaushik Roy (Cadence), replacing Eric M.
n[-----] Andrew Seawright (0-in)
n[--xxx] Bassam Tabbara (Novas)
n[-----] Tej Singh (Mentor)
n[x--x-] Connie O'dell (Consultant)
v[xxxxx] Hillel Miller (Motorola)
v[xxx..] Arif Samad (Synopsys - Co-chair)	
==||||+------------------------- 08/11/03
==|||+-------------------------- 08/08/03
==||+--------------------------- 09/15/03
==|+---------------------------- 09/22/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) Review extension proposals

Committee reviewed Surrendra's proposals (1.1 - 1.3) regarding
"assume" 


Section 1.1: Non-blocks Assignment (NBA) for Assertions

No comments

Adam

Section 1.2: Assumptions

Faisal requested some clarifications regarding the use of "dist"
to apply biasing to expressions within a property.

Surrendra explained how dist was used for dynamic simulation when
a property was used as an assumption. For assertions and for formal
verification "dist" was synonymous with inside.

Adam asked if there were any requests for temporal constraints?

Surrendra said that these were described in section 1.3

Adam asked whether assumes have to be in the program block.

Surrendra stated that they could be anywhere not just in program block.

Adam felt that there was a need for controls to specify which
block to create stimulus for?

Surrendra said that assumptions could be turned on or off
through a system task.

Adam asked whether this was through a new task or an existing task?

Surrendra said that this was through an existing task.

Joseph asked whether an assume "cut off" other signals driving the nets
in question.

Adam stated that he did do not like the idea that assume is only
used for one purpose.

Surrendra stated that the idea was to write properties which were
then controlled using the assert and assume directives.

Kausik sais that both assumptions and assertions were invariants and
asked what the difference was.

Surrendra explained that in formal verification assertions were
proved and assumptions were not. Simularly for simulations assume
was used to generate stimulus.

Adam stated that he would want testbench to explicitly say
where and what is driven.

John said that just having an assume on interior signals should
not lead to signals being driven.

Surrendra agreed that some other control was needed.

Arif asked whether having the tool infer the use of an assumption
based on whether it is on a primary input or an internal net
made sense.

John stated that his sounded reasonable but may not cover everything
that Adam had in mind.

Adam stated that he was concerned that a designer could accidently
put an assumption in and screw up the simulation. If the simulator
used assumptions to generate stimulus then this could interfere with
another tools using the assumption for a different purpose.

Joseph stated that this could occurs when assumptions at lower level
of the design became assertions at higher levels of integration.
He stated that there was a need to define a methodology.

There was some additional discussion regarding the use model for
assumptions and the need to control them.
call randomize.

The discussion was closed with the proposal that additional
discussions should be carried on offline.

Section 1.3: Using properties in the constraint block

Adam commented that the assume keyword was not used
when a property was used as in the constraint block.

Surrendra clarified that this was because the appearance
of the property in the constraint block implied that it
was to be used for stimulus generation.

Adam asked how cross-constraints were handled.

Arif explained that global constraints could be used to
specify constraints that spanned more than one object.

There was a question regarding whether there should be
a label per constraint. Arif explained that by having one
constraint per constraint block, one could get a label
per constraint.

There was some discussion of how randomization should
be synchronized with events rather then clocks.

Faisal proposed a built-in randomization event which
would be triggered when values were randomized.

Discussion was tabled in favor of offline discussion.