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.