RE: [sv-ac] #1381

Doron,

What Ed says below is exactly where 1381 and 805 do not mesh. Putting
aside whether it's a disabled (vacuous) success/fail/nothing, that's a
don't care, 805 does count these as disabled *attempts*. 1381 in current
form does not even consider these attempts.

From your email we have more agreement than difference so again this
binning *outside* of an attempt seems wrong, any kind of tracking has to
have an *attempt*. Sorry for repeating myself in many different ways --
thinking aloud, and can't converge on an understanding of where you are
at :). 

Thx.
-Bassam.

-----Original Message-----
From: Eduard Cerny 
Sent: Wednesday, May 10, 2006 12:58 PM
To: Doron Bustan; Bassam Tabbara
Cc: sv-ac@eda.org
Subject: 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
> >
> >  
> >
> 
> 
>