[sv-ac] P1800 SV-AC meeting , Tuesday, April 11 - collected comments regarding questions sent out yesterday

- Cover property on implication reporting: all successes or distinguish
vacuous from real.

BT&EC&SD> Distinguish: vacuous, match, also no-match (aka Fail). But it
could be left up to the tools.

DB&JH&LP> 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?

BT&EC&SD> Yes. Need to formally describe a vacuous match instead of
hiding in
text (e.g. applies at top level operator only), along with a description
of disable (see below). Need to review the new version proposed by
DB&JH.

DB&JH&LP> 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.)?

BT&EC&SD> No, it is a non-local change. If we distinguish then
clarification of vacuous should suffice. We could introduce it later,
syntactic sugar.

DB&JH&LP> 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?

BT&EC&SD> Result should be "disabled" i.e. no data collection i.e. "no
match".

DB&JH&LP> 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?

BT&EC&SD> No, it is a non-local change. Delay introduction.

DB&JH&LP> 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?

BT&EC&SD> Yes of course it should execute since we are associating a
"result"
with vacuous (success) and disable (fail or success (don't care)). Users
can choose to test the disable condition and/or check the system tasks
if they want to bypass execution. The default is execution (i.e. ON).
On covers active disable iff should not execute the action block.

DB&JH&LP> 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.



Additional comments:

Lisa Piper: I agree with John and Doron 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.