Re: [sv-ac] 805

Hi Lisa,

my answers below:


>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).
>
>  
>
I will change that to:

"In addition, statement_or_null is executed every time a property
is being evaluated to true."

Let leave the vacuous discussion to the "coverage" proposal.



>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)
>
>  
>
The proposal says in 17.11 that

"If prior to the completion of that evaluation the reset expression 
becomes true,  then the
overall evaluation of the property results in disabled."

in Annex E, we have a more precise definition using the |=d relation

The count is per attempt not per thread, so I am not sure what does it 
mean that
a thread is disabled?.


>By the way - that formula implies that there can only ever be one
>success per attempt - is that true?  
>
Yes

>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.
>
>  
>
There is a problem with the "cover property on a sequence" definition. 
If I understand
correctly, this is going to be fixed in the coverage proposal. The way I 
imagine
it, there will be a new directive "cover sequence" which will count 
sequences matches
not properties pass/fail.

>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.
>
>
>  
>
Manisha can you answer that?

>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.
>
>
>  
>
Manisha can you answer that?

>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?
>
>
>  
>

I am not sure here, my opinion is that disable_iff is part of the 
"logic" of SVA
and assert_off is more a "tool/testbench interface" feature, so I don't 
want to bring them
together. 


Doron