Dmitry, >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. > > Now I understand your point. Note, that with the current definition this will also not work for simulation, because we have not fixed the definition in the formal semantics. Adding a disabled status on the top level, means getting the disable iff out of the inductive definition, and adding the property_spec layer (currently not in the formal semantics) where we need to define the semantic of disable iff. we were thinking of something like $disable iff (b) P$ suceeds on computation $w$, iff either For every $i \geq 0$, $w^i \not \models b$ and $w\models P$ or Let $i$ be the minimal integer such that $w^i\models b$, then $w^{0..i-1}\cdot \bot ^\omega \models P$. $disable iff (b) P$ fails on computation $w$, iff either For every $i \geq 0$, $w^i \not \models b$ and $w\not\models P$ or Let $i$ be the minimal integer such that $w^i\models b$, then $w^{0..i-1}\cdot \top ^\omega \not\models P$. $disable iff (b) P$ is disabled on computation $w$, iff for some imteger $i$ we have that $w^i\models b$ and $w^{0..i-1}\top^\omega \models P$ and $w^{0..i-1}\bot^\omega \not\models P$ In english it means that "disable iff (b) P" succeeds if P holds before the first b "disable iff (b) P" fails, if P fails before the first b and "disable iff (b) P" is disabled otherwise. Doron >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. >>> >>> >>> >>> >>> >>> >> >> >> >>Received on Fri Jun 23 06:13:06 2006
This archive was generated by hypermail 2.1.8 : Fri Jun 23 2006 - 06:13:15 PDT