RE: [sv-ac] 805

Hi Lisa,

I try to give a first cut response to help clarify the basics, might
need further discussion.

** Doron: from quick skim typo "resrt" in 2 places instead of "reset". 


Thx.
-Bassam.

-----Original Message-----
From: owner-sv-ac@eda-stds.org [mailto:owner-sv-ac@eda-stds.org] On
Behalf Of Lisa Piper
Sent: Friday, July 28, 2006 10:15 AM
To: Doron Bustan; sv-ac@eda-stds.org
Subject: RE: [sv-ac] 805


1)  In 17.13.3:

REPLACE 
     In addition, statement_or_null is executed every time a property
succeeds.

WITH
     In addition, statement_or_null is executed every time a property
succeeds (this does not include vaccuous success or disabled).

**BT>> Sure, no harm in being more precise.

2) Am I correct that the disabled count is the number of attempts in
which disable iff is true?  It is not real clear based on the
terminology "reached the disabled state".  What happens when overlapping
threads from one attempt are disabled.  It would have to be the number
of attempts if the formula is true:  progress = attempts - (successes +
vacuous success + disabled + failures)

By the way - that formula implies that there can only ever be one
success per attempt - is that true?  That seems to conflict with the
"number of times matched (for cover property (sequence);)" on page 288
that specifically states that each attempt can generate multiple
matches.  If the above formula is wrong, then I am not certain that my
previous assumption is correct.

**BT>> 2 things. First the context of the formula is talking about
assertions only. Now in general particularly if you mean the assertion
API (which applies to all of assert/cover/prop/seq) I think it's fairly
clear than an "attempt" there really means (starttime, endtime, result),
I clarify more in (4) below. 

3) if in 29.4.3 we are adding the disabled count, then is there a reason
that it is not also part of the list in 17.13.3.

**BT>> Agreed, thx for pointing out thought we fixed this before. I
reiterate that we should treat "disabled" as another "result" and add
wherever needed.


4) 28.3.2:  is cb_time the time when it transitioned to the disabled
state?  in other words, if disabled is true for 3 consecutive attempts,
do I get 1 or 3 call backs.  Also, since disable iff is async, I assume
that what I get is really the time of the attempt.

**BT>> The cb_time is the time of the "result", so yes it would be the
real "async" time of the cb. The attempt start time has its own field
allowing you to get the tuple I mentioned before. So yes you do get 3 of
them.

5) it would be useful to comment of this "disabled" state compared to a
state that is reached as a result of assertoff system control task.  Is
there a difference other than how you get there?  Is there value in
differentiating?

**BT>> There already is differentiation, one is a "global" state, the
other is per attempt.

Lisa


-----Original Message-----
From: owner-sv-ac@eda-stds.org [mailto:owner-sv-ac@eda-stds.org] On
Behalf Of Doron Bustan
Sent: Friday, July 28, 2006 11:02 AM
To: sv-ac@eda-stds.org
Subject: [sv-ac] 805

Hi,

I added changes to annex E to the proposal and upload it to mentis.
Please look at the pdf version because the html versions are miisin a
few important characters.

I attached the pdf and the original word document