RE: [sv-ac] P1800 SV-AC meeting tomorrow, Tuesday, April 11.

I agree with John and Doran on all points. If I were defining this from
scratch, I would have said that vacuous counts are extraneous
information to most users and should not be required, however I think it
would be difficult to change at this point. Tools will likely have to
report both vacuous and non-vacuous.

Lisa Piper

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
Havlicek
Sent: Monday, April 10, 2006 5:17 PM
To: Eduard.Cerny@synopsys.com
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] P1800 SV-AC meeting tomorrow, Tuesday, April 11.

Ed:

Our answers are below.

DB & JH

> 
> Hello,
> 
> We need to close on the issue of cover property, followed_by.
> 
> There are several questions that we must address are:
> 
> - Cover property on implication reporting: all successes or
distinguish
> vacuous from real.

All successes should be reported.  It is o.k. for a tool to partition 
the successes into vacuous and non-vacuous.

We think it is important for success of cover property to be 
consistent with the property satisfaction relation.

> 
> - Doron and John proposed a definition of vacuity, should we take it
> into account at the same time?

We like our definition as modified as in the e-mail discussion.
We will update mantis with the revised definition.  Note that it
defines vacuous attempts, so it can be applied to successes or failures.


> 
> - Do we introduce followed_by at this time, which may require a
> non-local change (BNF, VPI, etc.)?

We don't think it is necessary, but we think it would help to avoid
bad coding of cover properties using implication.

> 
> - What is the effect of disable iff in a cover property/sequence?
> Vacuous vs. no match?

We think it is cleaner for disabled cover to be no match.  No one 
seems to want these counted as hits, nor do they want the action 
block to execute.

In the formal semantics, this requires treating disable differently
in a cover context from an assert context.  This is o.k. provided
disable is allowed only at the top level.  

> 
> - separate cover on sequences from those on property using a different
> construct? cover property vs. cover sequence?

We think that separate cover on sequences is a good way to distinguish
the "at most one match per attempt" semantics from the "all matches
per attempt" semantics.  

The key technical reason for this is that we think the multiplicity of
matching can be defined more easily for sequences than for properties.

However, we think that disable still needs to be allowed.  So some
thought needs to be given how to accommodate disable in this context.

> 
> - Should execution of action blocks depend on vacuity, disable? What
> should be the default?

Our users have been clear:

1. They do not want any action block to execute on a disabled attempt.

2. For an assert property, they do not want the pass action block to
   execute on a vacuous success.

If one were to write a cover property on a property that can
pass vacuously, we expect one would desire that the pass action 
block not execute on vacuous attempts.

> 
> - Other...?
> 
> 
> If you send me a brief message with your opinion on each of these
items
> by tomorrow morning ET, I will try to tabulate it before the meeting.
> 
> Note also that I entered a new errata (1420) regarding the passing of
> arguments  to recursive properties.
> 
> Best regards,
> ed
> 
>  
>