RE: [sv-ac] proposal for 1498

Hi Doron,

Of course, we are not talking about attempts in FV, and we need to use
the definition of an assertion success:

$w, b \models always @(c) assert property P iff for every 0 \le i < |w|
so that \overline{w}^i \models c and \overline{w}^i \models b,
w^{i..} \models @(c) P.

This definition won't work if the disabled attempts are not counted as a
success.

Thanks,
Dmitry

-----Original Message-----
From: Doron Bustan [mailto:dbustan@freescale.com] 
Sent: Thursday, June 22, 2006 9:18 PM
To: Eduard Cerny
Cc: Korchemny, Dmitry; john.havlicek@freescale.com; sv-ac@verilog.org
Subject: Re: [sv-ac] proposal for 1498

We took an action item to continue this discussion.
So let me explain my view:

In simulation there is a single computation with a finite number 
(usually less than 100,000)
of attempts. Thus it make sense to require the tool information per 
attempt (fail, disabled etc.)
and to execute tasks accordingly..

In formal, there are (potentially) infinitely many traces and attempts. 
Even in bounded model
checking where the number of computations and attempts is finite, the 
numbers can be way over
1,000,000,000 attempts, for relatively small depth as 50. Thus, we do 
not expect the tool to give
information per attempt, but only on the overall state of the design. In

particular for asserted properties,
we expect to know whether or not a failure was find.

The disable status of a property is relevant only per attempt , there is

no meaning to "property is disabled
design".  Since disabled is not a failure, we should not expect
a formal tool to report it.



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