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