Minutes of IEEE P1800 SV-AC meeting #2006-6: 03/28/2006
Written by: Ed Cerny

Code for the conference call:

        Domestic:         888-635-9997
        International:    763-315-6815
        Participant code: 2638198

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

n[xxx-x-] Faisal Haque (Cisco, Chairman)
v[xxx-xx] Eduard Cerny (Synopsys - Co-chair)	
v[xxxxxx] John Havlicek (Freescale)
v[xxxxxx] Doron Bustan (Freescale)
v[xxxxxx] Manisha Kulshrestha (Mentor Graphics)
v[xxx---] Volkan Esen (Infineon)
v[-xxx-x] Bassam Tabbara (Synopsys)
v[-xxxx-] Hillel Miller (Freescale)
v[-x--xx] Surrendra Dudani (Synopsys)
v[-xxxx-] Joseph Lu (Altera)
 [.x-x--] Yaniv Fais (Freescale)
v[..xxxx] Dmitry Korchemny (Intel)
 [....xx] Lisa Piper (Cadence)
=======|---------------------------- 03/28/2006

Agenda:
-------

- Review IEEE working group rules
- Review errata reported in Mantis


Minutes:
--------



1) Discussion about cover property semantics in the presence of
disable if and vacuous successes due to implication. Introduction of
followed_by as the dual operator of |-> and |=>, useful in cover
properties (it is a syntactic sugar because the operator can be
expressed as "not ( s |-> not p)" ). Related to issues #1383, #805 and
#1361.

Summary of the discussion: 

Should cover property on an implication report only all successes or
distinguish vacuous from real successes? The former would make it
different from assert property, but may be more inductive for user to
employ followed_by instead of implication. A possible solution may be
that by default it counts all successes, but the tools and VPI will
provide mechanisms to access the different subcases - vacuous,
non-vacuous.

There seems to be agreement that disable iff on a cover property
should count as no match rather than a vacuous success. That is, the
semantics change from assert to cover.

Followed_by as a dual operator to implication should be
introduced. However, this is an enhancement that may affect several
areas in the LRM. Must verify to what extent such a change can be
voted on at this point in time.

There is an agreement that a cover on a sequence with its "all
matches" semantics should be specified using a different directive,
namely "cover sequence".

What should be done about the control of action blocks in the presence
of disable iff and vacuous successes? This can be solved once it is
agreed on what to do with cover property on an implication. To be
discussed at the next meeting.

2) Results of email vote on issue #1346: 7 for, 0 against. Approved.

3) Action items before next meeting: come to a conclusion by email
about the above issues so that we can close on it.

Next meeting: 04/11/2006 at 9 am PT (12 pm ET, 6 pm Europe).
====