Re: [sv-ac] #1381

I don't think this should be part of the vacuity proposal. This is just 
an explanation
why I didn't add the "final form of the inferred assertion in SVA".

I think that we should decide on the exact semantics of coverage in the 
future
coverage proposal, the followed_by can come later (we can used "not 
(R|-> not P)"
until then

It would be good if we would be able to vote on 1831 now, so I don't 
want it
to depend on the coverage discussion.

Doron


Eduard Cerny wrote:

>I like followed_by and did want to have it, but if we should not make
>cover and vacuity dependent on it, i.e., not introduce a new keyword
>now. This is what Doron proposes which is ok as it uses the existing
>operators. I just wanted to minimize the changes, by leaving how the
>condition is extracted for embedded covers and control it on the
>reporting side only. 
>ed
>
>
>  
>
>>-----Original Message-----
>>From: Bassam Tabbara 
>>Sent: Wednesday, May 10, 2006 6:53 PM
>>To: Doron Bustan; Eduard Cerny
>>Cc: Bassam Tabbara; sv-ac@eda.org
>>Subject: RE: [sv-ac] #1381
>>
>>Sure this proposal can cover :) that too -- I forget if there was a
>>separate mantis item for followed_by. As Doron/Dimitry noted 
>>#805 needs
>>an update in this respect too.
>>
>>Thx.
>>-Bassam.
>>
>>-----Original Message-----
>>From: Doron Bustan [mailto:dbustan@freescale.com] 
>>Sent: Wednesday, May 10, 2006 3:35 PM
>>To: Eduard Cerny
>>Cc: Bassam Tabbara; sv-ac@eda.org
>>Subject: Re: [sv-ac] #1381
>>
>>I think that the user should have at least the option to 
>>report "vacuous
>>successes" for coverage. I would prefer that we will not 
>>define vacuity
>>for coverage at the first place, but at least have the option 
>>to ignore
>>it.
>>
>>For this option we need the followed_by
>>
>>Doron
>>
>>Eduard Cerny wrote:
>>
>>    
>>
>>>Hi Doron, Bassam,
>>>
>>>Currently it is also an implication rather than a 
>>>      
>>>
>>followed_by. I guess 
>>    
>>
>>>it does not matter if the reporting and execution of action blocks 
>>>would ignore vacuous successes. So, do we need to change to
>>>      
>>>
>>followed_by?
>>    
>>
>>>ed
>>>
>>> 
>>>
>>>      
>>>
>>>>-----Original Message-----
>>>>From: Doron Bustan [mailto:dbustan@freescale.com]
>>>>Sent: Wednesday, May 10, 2006 4:26 PM
>>>>To: Eduard Cerny
>>>>Cc: Bassam Tabbara; sv-ac@eda.org
>>>>Subject: Re: [sv-ac] #1381
>>>>
>>>>Ed, Bassam,
>>>>
>>>>I don't think it is so important, (but it should be defined).
>>>>So if no-one else will comment on that in the next few days, I will 
>>>>change the proposal, such that there is an attempt for every 
>>>>evaluation of the condition in the procedural code.
>>>>
>>>>do you agree that for coverage, the semantic should be
>>>>
>>>>cover property (@(clk) not (a |-> not p); //(a followed_by p) ?
>>>>
>>>>
>>>>thanks
>>>>
>>>>Doron
>>>>
>>>>Eduard Cerny wrote:
>>>>
>>>>   
>>>>
>>>>        
>>>>
>>>>>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
>>>>>
>>>>>
>>>>>     
>>>>>
>>>>>          
>>>>>
>>>>Bassam Tabbara wrote:
>>>>
>>>>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.
>>>>
>>>>
>>>>
>>>>   
>>>>
>>>>        
>>>>
>>> 
>>>
>>>      
>>>
>>    
>>
>
>  
>