RE: [sv-ac] proposal for 1498

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