RE: [sv-ac] 805

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