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

SV-AC v3.1a Meetings:
        Next meeting October 13 9am PST

Note: new number:

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[xxxx] Faisal Haque (Cisco, Chairman)
v[xxxx] Arif Samad (Synopsys - Co-chair)	
n[xx-x] Roy Armoni (Intel)
v[xxxx] Surrendra Dudani (Synopsys)
n[----] Cindy Eisner (IBM)
v[xxxx] John Havlicek (Motorola)
n[----] Richard Ho (0-in)
v[xxx-] Adam Krolnik (LSI)
v[xxx-] Joseph Lu (Sun)
n[-x--] Rishiyur Nikhil (Blue Spec)
v[-x-r] Kaushik Roy (Cadence), replacing Eric M.
n[----] Andrew Seawright (0-in)
n[---x] Bassam Tabbara (Novas)
n[----] Tej Singh (Mentor)
n[-x--] Connie O'dell (Consultant)
v[xxxx] Hillel Miller (Motorola)
==||||+------------------------- 09/08/03
==|||+-------------------------- 09/15/03
==||+--------------------------- 09/22/03
==|+---------------------------- 09/29/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

Correction to 9/22/03 Minutes
-----------------------------
- Attendance should have indicated that Rishiyur Nikhil from
  BlueSpec was present


Misc
----
- John: Problem with getting special symbols using Frame (Formal symbols).

Discussion on "assume" extension
--------------------------------

Roy- in general adding assumptions to SVA is a good choice. Want to
first consider what the methodology. Traditionally this is used for
assume/guarantee. Don't see Surrendra's proposal as being exactly
this.

Surrendra: tools can interpret based on what the application is.
If you wanted to make the same property as assumption in one application
and assert in another could use bind. Put properties outside the block
and use bind to make them assertions or assumptions.

Second way leave it to the tool to decide whether an assumption is used
as an assertion or assumption.

Roy: want to propose something more explicit. Prune out logic and leave
something that tool can handle. Put assumptions to model pruned logic.
In the complete model that includes pruned logic assumptions must hold.
This suggests that FV would use assumptions as restrictions on the
environment. In simulation where complete model is available assumptions
should hold - should check them in simulation.

In order to do stimulus generation, propose an additional directive that
would constrain stimlulus or use for case generation in FV - something
like "restrict"

Roy: Propose assume generate proof obligation.
Additional keyword restrict for case splitting in FV or some restriction
for stim gen.

John: concern: want to understand rationale.

Want stim gen to meet assumptions. When combine block with
another block want assumptions to be checked.

How will use restrict for this?

Roy: do test generation for block only?

John: yes. Could be preliminary verification before FV on block.

Hillel: what do we need restrict for.

Roy: case splitting.

Surrendra: could this be accomplished by an attribute rather than
a separate directive.

Roy: everything could be done with an attribute. Even the assume.
The question is whether this feature is important enough to 
justify a new keyword in the language.

John: like the idea of separating pure assumption that must hold
from temporary or ad-hoc case splitting assumption.

Surrendra: how would the restrict work in random generation.

Roy: it would be applied to test generation also.

Restrict used for stimulus generation at the block level.
Ignored when block is incorporated into system.

Assume is used to constrain stimulus + check at higher level.

Joseph: if assume is put between two blocks A->B, it is checked. What
happens to restrict?

Roy: when block is incorporated into system case splitting is no
longer needed. Don't need restrict anymore.

John: like the idea of having a separate syntax to describe 
assumptions that only hold for blocks.

What is not clear is when something that is used for an 
assume is used for test generation or checking.

Depending on how blocks are combined an assumption could be
used for stimulus generation or checking.

Joseph: Tool would have to recognize this. Need to define guidlines

Arif - doesn't this seem reasonable?

John: need analysis to make sure that nets are primary inputs
or reachable though combinational logic.

Hillel: couldn't we just treat an assumption as an assertion once
a block is incorporated into a higher level.

Joseph: for prev project - provided guidance to tool as to what level
to go to figure out whether to drive or check.

Surrendra: question regarding restrict: How to handle case when some
of the inputs with a restrict are free?

Roy: when there is a full model ignore restricts.

Surrendra: does the tool know when there is a full model.

When everything is hooked up ignoring restrict is easy. Problem
is when there are free inputs that have a restrict.

Roy: concentrate on assume directive first. Just wanted to note
that there are other options for constraining values for test
generation - the restrict. Deciding that the interpretation of
the assume directive is tool dependent leaves too much freedom.

For the assume directive should describe use model and rationale.

Surrendra: will add this to his proposal.

Surrendra: create time table for consideration of all the proposals.

Discussion on Surrendra Proposal "1.4, 1.5" in PDF file
-------------------------------------------------------
Allow message in assertion itself using $info, $warning, $fatal, $error

John - likes this because don't know how to solve the multi-thread to 1
problem...

Adam: have to invert the sense of the property to get the failing
message. This could make it more confusing.

Surrendra: agrees.

Adam: if we could put the error message inside the property. That would
be a better approach. Don't know how to propagate the value to it.

John: Hillel made the comment that any thread that executes it
call the $display. This is ok.

If the property failed would know what the values are in that thread.

Adam: could we attach a message to the end of the property.

Surrendra: could. Could put ##0 and put $info at the end.

John: property could be failing before the end.

Surrendra: attaching a message to the property would solve
that but would not solve the local variable problem.

John: need some more brainstorming on this. Want to execute
display when failure happens.

Surrendra: like action block.

John: except want it for every thread.
Could we change action block to accomplish this -
else action block...1.4 Access to Sampled Values

Adam: volunteer to write up a summary of the problem
and possible ways to address - try for this week.

Adam: can we go back more than one cycle?

Surrendra: can extend $past. Difficult to mix $past in the middle
of expressions that are event

$past - expression as well as variable. Method would only work for
a single variable.

Discussion on Surrendra Proposal 1.6 Passing Unbounded Range
------------------------------------------------------------
Surrendra: create example.