RE: [sv-ac] #1381

I am not sure that not countying "attempts" for embedded assert property
when the condition is false is a good idea. This is just a syntactic
structure and the effective one is the extracted one into a concurrent
assertion. If one extracts it manually or let the compiler do it, the
behavior should be the same. I.e., have the same evaluation attempts,
even if vacuous. 

ed 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Doron Bustan
> Sent: Wednesday, May 10, 2006 3:54 PM
> To: Bassam Tabbara
> Cc: sv-ac@eda.org
> Subject: Re: [sv-ac] #1381
> 
> Bassam,
> 
> >** One more suggestion: Add a sentence that shows the final 
> form of the
> >inferred assertion in SVA constructs to make this clear.
> >  
> >
> I think that for assertions
> 
> always $(clk) if (a) assert property (p);
> 
> should be logical equivalent to
> 
> assert property (@(clk) a |->p)
> 
> but with less evaluation attempts of the assertion, because the
> "a" condition is part of procedural code and not the assertion.
> On the other hand, the cover property
> 
> always $(clk) if (a) cover property (p);
> 
> should be logical equivalent to
> 
> cover property (@(clk) not (a |-> not p)
> 
> again with less evaluation attempts of the property, because the
> "a" condition is part of procedural code and not the assertion.
> 
> 
> >** My opinion: I think we are dropping a valuable piece of 
> information
> >-- namely the disabled (don't care if it's marked a success or fail
> >really). In my mind, why am I inferring the condition if I 
> don't want to
> >"report" it somehow. If I am ignoring it then let's not infer it into
> >assertion to begin with ...
> >
> 
> This proposal does not cancel any information on disable, it 
> only define 
> disabled
> evaluation as vacuous.
> 
> >
> >---> Recap: this proposal should be tied to #805 (and any other new
> >coverage issue/proposal) -- they have to be consistent. 
> Today's #805 and
> >this proposal do not mesh.
> >  
> >
> Bassam, can you be more specific, I don't see how this proposal 
> contradict proposal 805.
> 
> thanks
> 
> Doron
> 
> >Bassam Tabbara wrote:
> >
> >  
> >
> >>I vote yes.
> >>checking my notes I find couple of comments:
> >>
> >>- typo extra "the" on page 2 (c). 
> >>
> >>- page 3 last sentence before 17.13.5. "... a new 
> evaluation attempt of
> >>    
> >>
> >the underlying property_spec begins ..."
> >  
> >
> >
> >I fixed the first two items, I will upload it later today.
> >
> >  
> >
> >>- page 3 section 17.13.5 added sentence "A concurrent assertion ..."
> >>    
> >>
> >makes it seem that an attempt only starts (at every clock event) when
> >the enabling condition holds, sentence needs rewording (the semantics
> >are ok).
> >  
> >
> >> 
> >>
> >>    
> >>
> >I don't think that there should be an attempt if the 
> condition does not
> >hold, I know that it does not fit the implication attempt 
> semantics, but
> >we will have to change that for coverage anyway.
> >
> >Doron
> >
> >  
> >
> 
> 
>