Re: [sv-ac] proposal for 1498

Dmitry, Ed,

Since we expect formal tools to report only failures (not disabled and 
not vacuous),
I don't think this is a problem.

Doron

Eduard Cerny wrote:

>Sounds reasonable.
>ed 
>
>  
>
>>-----Original Message-----
>>From: owner-sv-ac@eda-stds.org 
>>[mailto:owner-sv-ac@eda-stds.org] On Behalf Of Korchemny, Dmitry
>>Sent: Monday, June 19, 2006 9:36 PM
>>To: john.havlicek@freescale.com
>>Cc: sv-ac@verilog.org
>>Subject: RE: [sv-ac] proposal for 1498
>>
>>Hi John,
>>
>>I see a problem in defining a property status as disabled. I 
>>think that
>>from the formal point of view each property should either pass or fail
>>on infinite words. Otherwise, it will impose an unnecessary burden on
>>formal tools to check whether a property has succeeded 
>>because of reset.
>>Of course, vacuity checks are important for FV, but they should not be
>>compulsory.  Wouldn't it be easier to leave the formal 
>>semantics as is,
>>but to define when action block should be performed?
>>
>>I think that coverage should not report property failures at all, thus
>>the only question remains for pass action execution of 
>>assertions. They
>>may be controlled with $assertdisabledon/off from Manisha's proposal.
>>
>>Thanks,
>>Dmitry
>>
>>-----Original Message-----
>>From: John Havlicek [mailto:john.havlicek@freescale.com] 
>>Sent: Friday, June 16, 2006 3:27 PM
>>To: Korchemny, Dmitry
>>Cc: sv-ac@verilog.org
>>Subject: proposal for 1498
>>
>>Hi Dmitry:
>>
>>I looked over your proposal for 1498 and noticed a couple of 
>>things in relation to Manisha's proposal for 0805.
>>
>>In Manisha's proposal, the result of a disabled attempt is
>>neither pass nor fail.  This treatment of the disabled attempt
>>is involved with preventing the following undesirable things:
>>
>>1. Pass action block executing on disabled attempt.
>>2. Disabled coverage property attempt counting as a hit.
>>3. Disabled assert property attempt counting as a non-vacuous
>>   success.
>>
>>In 1498, you propose to introduce accepton and rejecton in the 
>>formal semantics and translate "disable iff" either into accepton
>>(in the case of an assert property) or "rejecton" (in the case of
>>a cover property).
>>
>>Your proposal would say, I think, that a disabled assert property 
>>attempt is a vacuous success, while a disabled cover property 
>>attempt is a failure.
>>
>>Manisha's proposal says that the disabled attempts are separate
>>from successes and failures.
>>
>>Manisha points out that by saying that disabled attempts are neither
>>successes nor failures, less LRM text needs to be changes to 
>>avoid undesirables 1-3 above.  I think this also will make it easier
>>to teach users how to understand for which attempts the action blocks 
>>execute.
>>
>>But then in the formal semantics I think we must not transform
>>"disable iff" into accetpon or rejecton.  Instead, we need a separate
>>definition like the following:
>>
>>   Let u be the longest prefix of w such that no letter of u satisfies
>>b.
>>   Then 
>>   
>>      w |= disable iff (b) P  iff  u\bot^\omega |= P
>>      w |/= disable iff (b) P  iff  u\top^\omega |/= P
>>   
>>   Otherwise evaluation of "disable iff (b) P" on w is disabled.
>>
>>[This definition is in the spirit of the current formal semantics 
>>and does not attempt to solve the known problems with the \top,\bot
>>approach to reset semantics on unsatisfiable formulas.]
>>
>>And, as I pointed out before, this means that "disable iff" needs
>>to be kept always at the top level [unless, e.g., a 3-state inductive 
>>semantics is defined].
>>
>>Best regards,
>>
>>John H.
>>
>>
>>    
>>
>
>  
>