Re: [sv-ac] proposal for 1498

Hi Dmitry:

If the disabled attempts are not counted as successes or failures, 
then this definition needs to be changed.  Annex E should move 
disabled out of the recursive syntax and adjust the definitions
for the assertion directives to exclude disabled attempts from
passing or failing.

J.H.

> X-IronPort-AV: i="4.06,166,1149490800"; 
>    d="scan'208"; a="56164968:sNHT58095947"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Fri, 23 Jun 2006 01:52:26 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] proposal for 1498
> thread-index: AcaWKW9A6zEbGNY0RTyvuEW3ZJSHuQAJD8pw
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: <john.havlicek@freescale.com>, <sv-ac@verilog.org>
> X-OriginalArrivalTime: 22 Jun 2006 22:52:30.0934 (UTC) FILETIME=[8AF18F60:01C6964E]
> 
> 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]=20
> 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=20
> (usually less than 100,000)
> of attempts. Thus it make sense to require the tool information per=20
> attempt (fail, disabled etc.)
> and to execute tasks accordingly..
> 
> In formal, there are (potentially) infinitely many traces and attempts.=20
> Even in bounded model
> checking where the number of computations and attempts is finite, the=20
> numbers can be way over
> 1,000,000,000 attempts, for relatively small depth as 50. Thus, we do=20
> 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=20
> >
> > =20
> >
> >>-----Original Message-----
> >>From: owner-sv-ac@eda-stds.org=20
> >>[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=20
> >>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=20
> >>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=20
> >>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=20
> >>assertions. They
> >>may be controlled with $assertdisabledon/off from Manisha's proposal.
> >>
> >>Thanks,
> >>Dmitry
> >>
> >>-----Original Message-----
> >>From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> >>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=20
> >>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=20
> >>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=20
> >>attempt is a vacuous success, while a disabled cover property=20
> >>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=20
> >>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=20
> >>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=20
> >>  =20
> >>      w |=3D disable iff (b) P  iff  u\bot^\omega |=3D P
> >>      w |/=3D disable iff (b) P  iff  u\top^\omega |/=3D P
> >>  =20
> >>   Otherwise evaluation of "disable iff (b) P" on w is disabled.
> >>
> >>[This definition is in the spirit of the current formal semantics=20
> >>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=20
> >>semantics is defined].
> >>
> >>Best regards,
> >>
> >>John H.
> >>
> >>
> >>   =20
> >>
> >
> > =20
> >