Minutes SV-AC 10/27/03
Written by: Arif Samad

SV-AC v3.1a Meetings:
        Next meeting November 3 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[x-xxx] 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[xx-xx] Adam Krolnik (LSI)
v[xxxxx] Joseph Lu (Sun)
n[---x-] Rishiyur Nikhil (Blue Spec)
v[x-x-x] Koushik Roy (Cadence)
n[-----] Andrew Seawright (0-in)
v[xxx--] Bassam Tabbara (Novas)
n[-----] Tej Singh (Mentor)
n[--x-x] Connie O'dell (Consultant)
v[x-xxx] Hillel Miller (Motorola)
==||||+-------------------------- 09/22/03
==|||+--------------------------- 09/29/03
==||+---------------------------- 10/13/03
==|+----------------------------- 10/20/03
==+------------------------------ 10/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) Action Items

From 10/20/03
* John: break up his proposal to separate discussion 
  of nested implications and boolean connectives.No need
  to provide detailed instructions for LRM changes

Status: working on it.

* John: add the proposal for if-then-else construct in the
  boolean connectives proposal for properties 

Status: working on it.

* 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 

Status: planning to do at chair's meeting.

From 10/27/03
* Surrendra - More information on formal semantics of assume.

* Surrendra - add text to describe that assumptions will be
  checked in simulation.

* Surrendra - examples for using assume in constraint blocks

* Arif - add Adam's erratum to list. Have committee review.

2) Minutes

Discussion on Surrendra's proposal numbered 1.2: Assumptions
------------------------------------------------------------
Surrendra went over proposal followed by discussion.

Key questions raised by discussion:

- Are assumptions checked in simulation and formal verification?
- If so, under what conditions? What role do "free variables"
  play in determining this?
- Is additional construct "restrict" needed?

After discussion, no definitive conclusion was reached.
There seemed to be general agreement that assertions
should be checked in simulation. There was not as
clear a view about how they should be treated in
formal verification.

Details:

Faisal: difference between this and use of assume in 
constraints?

Surrendra: don't randomize explicitly - tool does it automatically
Tool should specify additional controls - e.g.
what point in the cycle randomization should be performed.

Faisal: what about transaction level?
Surrendra: use events for clocking (?)

Adam: should assume be like a guarantee in PSL?

Surrendra: there were suggestions for additional directives such as
restrict from Roy.

Adam: we need to pick what kind of assume this is. Can see
uses for both. Are you more interested in using this as a 
non-guaranteed assumption?

Several: Does assume imply proof obligation or not for formal tools?

Surrendra: should be left to the tool.

John: on the biasing - what this be applicable to what one does with
classes as well?

Surrendra: syntactically it is the same.

John: if this is only for taking a bunch of signals and randomizing
them then don't see that it is that powerful.

Surrendra: simplified way to randomize signals.

John: see this as having limited utility unless it is related to classes.

Surrendra: this would be used when properties are attached to the
block. Need to have biasing if assume is to be used for random simulation.

John: is biasing allowed in temporal range?

Surrendra:no - just values.

John: it would be useful to be able to have distributions for temporal
ranges.

Adam: concerned that this would change the way properties are represented.
Upto now ranges are compile time constants.

John: distribution is supposed to be a hint to stimulus generator.

Adam: what is being randomized is not a signal value but an assertion
structure...

John: don't see that. Biasing is just determining what choices are being
made within the scope of the definition.

Adam - want to see assume as something that is checked. 

Faisal - might get triggered if do exception testing

Joseph - turn assumes into monitors for simulation

Surrendra: should assumptions be assertions for simulation?

Adam: do we have to say additional things to map to PSL?

John: don't remember what PSL says about difference between assume and assume
 guarantee

Joseph: assume guarantee - direction to the tool to check that assumption holds.
Just assume - no obligation to guarantee.

Arif - see free variables as a netlist propert. Does a tool look at an assume,
see that is on non-free variables and then treat it as an assert?

Surrendra: for simulation assume on non-free variables should be checked.

Hillel - should we declare free variables?

John - want to do a formal analysis that the assumptions on block B are
met by Block A...

Adam - distinguish between assumes that are in RTL versus those that
are included in an external file.

Arif - are we agreed that assume are to be checked?

Surrendra - yes for simulation, not for formal.

Arif - not sure see the difference based on what John was talking
about...

Surrendra - restrictions help formal tools to deal with capacity.

John - do we want restrictions?

Adam - don't see putting restrictions into RTL. Could just put into
a run file.

Joseph - if assume can be attached with a name in separate file

Adam - how do people use CBV - put assertions in separate file?

Hillel - assertions are in separate file. Convert constraints into assertions.
Don't put them in RTL.


1.3: "Using Properties in the Constraint Block"
----------------------------------------------

Surrendra went over his proposal to use properties
as constraints within a class. 

There was general discussion on this:

The key points were:

- how does this differ from the use of assumptions as
  constraints; when are values assigned?
- how is this used at the transaction level?

Because of time constraints, this discussion could not
be completed. Surrendra will provide more information
to clarify usage of properties as constraints.

Next Meeting
------------
- Discuss Adam's erratum
- Complete Surrendra's proposals.