Re: [sv-ac] 805

From: Doron Bustan <dbustan_at_.....>
Date: Fri Jul 28 2006 - 13:09:19 PDT
I agree, but still I think it should be part of the coverage proposal.

Doron

Eduard Cerny wrote:

>I think that we also must consider when the action block executes on
>coversequences. As much as it increments on each match (not just first
>match) of an attempt, the action block should also execute on each
>match.
>
>ed
> 
>
>  
>
>>-----Original Message-----
>>From: owner-sv-ac@eda-stds.org 
>>[mailto:owner-sv-ac@eda-stds.org] On Behalf Of Kulshrestha, Manisha
>>Sent: Friday, July 28, 2006 2:30 PM
>>To: Doron Bustan; Lisa Piper
>>Cc: sv-ac@eda-stds.org
>>Subject: RE: [sv-ac] 805
>>
>>My answers are included. 
>>
>>-----Original Message-----
>>From: owner-sv-ac@server.eda-stds.org
>>[mailto:owner-sv-ac@server.eda-stds.org] On Behalf Of Doron Bustan
>>Sent: Friday, July 28, 2006 11:00 AM
>>To: Lisa Piper
>>Cc: sv-ac@server.eda-stds.org
>>Subject: 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?
>>
>>Manisha: As far as I remember from our previous discussions 
>>with Bassam,
>>the section 29.4.3 describes vpi routines which apply to 
>>assertions (not
>>covers). That is why we included it there. But we did not 
>>want to report
>>disable counts for covers.
>>
>>    
>>
>>>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?
>>
>>Manisha: Based on my understanding, you will get three callbacks (this
>>has been discussed before with Bassam). If disable is true at the time
>>of attempt, you will get the time of the attempt as cb_time.
>>
>>    
>>
>>>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
>>
>>
>>    
>>
>
>  
>
Received on Fri Jul 28 13:09:26 2006

This archive was generated by hypermail 2.1.8 : Fri Jul 28 2006 - 13:09:30 PDT