Minutes SV-AC 02/25/03
Written by: Stephen Meier

ATTN: Next SV-AC Meeting Th March 6th 9:30-10:30AM PST 
	Dial-In = 888-830-6260
	Intl: 1-505-242-2420
	PartID = 908704

Legend:
x = attended
- = missed
r = represented
. = not yet a member
v = valid voter (3 out of last 4)
n = not valid voter

v[xxxxxxxxxxxxx----x.] Faisal Haque (Cisco, Chairman)
v[xxxxxxxxxxxxx-x-x-x] Steve Meier (Synopsys, Co-Chair)
v[-xxxxxxxxxxx-xxx--x] Roy Armoni (Intel)
v[xrxxxxxxx-x-xxxrxx.] Surrendra Dudani (Synopsys)
v[xxxxxxxxxxxxxxxrxrx] Cindy Eisner (IBM)
v[xxxxxxxxxxrxx-xxx..] John Havlicek (Motorola)
v[xxrxxxxxx-xx-xxxxx.] Richard Ho (0-in)
v[-xxxx-xxxxxxxxxxrx-] Adam Krolnik (LSI)
v[xxxx-xxxxxxxxx---xx] Joseph Lu (Sun)
v[-xxxxxxxxxxxx--xxxx] Erich Marschner (Cadence)
v[xxxrxxxx-x-xxxxxx-x] Andrew Seawright (0-in)
v[xxxxxxxxxxxx-xrxxxx] Bassam Tabbara (Novas)
v[-xxxx-x-xxxxx-xxxx-] Prakash Narain (Real Intent)
v[-xxxxx.............] Tej Singh (Mentor)
v[-xxxx..............] Connie O'dell (Consultant)
v[-xxx-x--xxx-x--xx-x] David Lacey (HP, OVL Chairman)
v[xxxx---x...........] Hillel Miller (Motorola)

n[xx.................] Kurt Shultz (Motorola)
n[---xx-xxx-rx-xxxrrx] Harry Foster (Verplex)
n[----xx-----xxxxxxx.] Ambar Sarkar (Paradigm Works)
n[------xxxxx........] Yaron Wolfsthal (IBM)
n[-----x.............] Glenn Wesley (Consultant)
n[-------xxx-xxxxxxxx] Gail Dagan (Intel)
n[--------xxxxxxxxxx-] Rajeev Ranjan (Real Intent)
n[---------x.........] Sagi Katz (Gallileo)
n[--------xxxx-x-x...] Richard Stolzman (Verplex)
n[-------xxx-xxxxxxrx] Tom Fitzpatrick (Synopsys)
n[-------x--x-x-x--xr] Tom Anderson (0-in)
n[------------------x] Jason Andrews (Axis)
==||||||||||||||||
==||||||||||||||||+- 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

1. Ballot Review

Ballot items were reviewed and issue list was updated.

2. New Issues

New Issue 15: Restricitons on directives in procedural context: Cindy, 2nd John, 3rd Joseph:
---------------------------------------------------------------
Procedural context, issue is when in procedural context neither always nor initial should be permitted at the procedural level.  Always is explicitly required at declarative level, then semantic restriction within procedural.

Cindy's concern is with:
	if ( abc) assert always ( x ; y ; z)

which in REv0.8 when extracted would translate into
	assert @(posedge clk) always (abc => x;y;z)

the concern that Cindy has it that the syntax might imply something different to experience
users of formal languages like the following:
	assert @(posedge clk) always (abc => always (x;y;z))

Cindy will document with written proposal (by Friday).

New Issue 13: Multiple clock support: Joseph, 2nd by Roy and 3rd by Hillel
-------------------------------------
Joseph is concerned about specifiying properties across multiple clock domains.  He put a preliminary requirement.

1) Proposal to use 1 clock within a specific sequence, use sequence implication and matched as means to cross clock domains.  John indicated the semantics have been written down in OVA semantics document, and feels that the semantics can be defined.  Cindy would like to undestand, Steve will send out OVA semantics document.

Cindy asked if Joseph's proposal is same as removing semantic restriction on sequences not using multiple clocks.  Steve clarified that it only removes restriction for sequence implication and matched operator.

2) Need to address the operational semantics of resolving the total order of events from partial-ordered sequences which are across multiple clocks.

Joseph indicates that if there is a cycle in the ordering and that would be cycle.
John indicated that he envisions a strict point of view and if there is a loop at compile time then it would cause an error.  

Issue needs more analysis, Joseph will send an example.

3) How to associate asynchronous clocks to the simulation ticks (atomic ticks)?

Steve indicated he feels there is a way to have a clock generator which toggles on
every simulation tick.  Joseph is ok with this resolution.

4) At which clock sampling point a sequential implication fails or holds if
    multiple clocks are involved.

Joseph considers when endpoint of LHS of seqa => seqb occurs simultaneously with seqb.  The semantics for this needs to be established.  John indicated that it can be written several ways.
John, Joseph and Surrendra will discuss proposal and semantics to support.

2. Discussion Points

Note:  Friday all hands meeting

Scheduling Semantics
====================
The scheduling semantics is strictly about evaluation steps within dynamic simulation.  It forms
the basis for how traces of sampled signals will be extracted for analysis by assertion
engines.  It also indicates where the pass/fail conditions of assertions are evaluated.

It is my understanding that it is fully compatible (but more general) with the sampling
semantics outlined in DWG and in the SVAC 0.79 version, but the terminology is different.

The scheduling semantics defines how traces are extracted and the assertion semantics defines how the traces are analyzed as assertions, so the semantics are separate but rely on both having clear definitions.

The scheduling working group has considered assertion requirements on both the
design and verification code.

Meeting Concluded