Hi John, I really like all your suggestions very much. I updated the proposal and uploaded it to Mantis. If you call for vote, it should be noted that FormalFuture_071022_dk.pdf is also part of this proposal. Thanks, Dmitry -----Original Message----- From: John Havlicek [mailto:john.havlicek@freescale.com] Sent: Wednesday, December 12, 2007 8:53 PM To: Korchemny, Dmitry Cc: sv-ac@eda.org; Bustan, Doron; eduard.cerny@synopsys.com; yaniv.fais@freescale.com; john.havlicek@freescale.com; Korchemny, Dmitry; Manisha_Kulshrestha@mentor.com; johan.martensson@jasper-da.com; piper@cadence.com; Seligman, Erik; bassam.tabbara@synopsys.com; thomas.thatcher@sun.com Subject: suggestions for 1682 Hi Dmitry: Below are my suggestions for revising 1682. I have copied the SV-AC actives so that they can comment. I don't yet have evidence that the SV-AC reflector is yet working. J.H. ------------------------------------------------------------------------ ----------- * p. 1. I don't think that the italics should be used in "They can only be used when global clocking is defined". I recommend setting this in ordinary roman and change to something like If a global clocking past or future sampled value function is used, then global clocking shall be defined or They may be used only if global clocking is defined * I recommend rewriting An evaluation attempt of an assertion containing global clocking future sampled value functions ends at the global clocking tick that follows the assertion clock tick at which the final boolean expression of the assertion is evaluated. This allows the evaluation of the global clocking future sampled value functions to be delayed until after the next values of the referenced signals have been computed. Note however, that the behavior of the disable iff clause and other asynchronous assertion related controls (e.g. $assertkill, see 19.10) remains consistent with its behavior for assertions without global clocking future sampled value functions (see 16.12): the completion of the property evaluation does not include (or is not contingent on) the additional global clocking tick. as Even though global clocking future sampled value functions depend on future values of their arguments, the interval of simulation timesteps for an evaluation attempt of an assertion containing global clocking future sampled value functions is defined as though the future sampled values were known in advance. The end of the evaluation attempt is defined to be the the last tick of the assertion clock and is not delayed any additional timesteps up to the next global clocking tick. The behavior of disable iff and other asynchronous assertion related controls such as $assertkill (see 19.10) is with respect to the interval of the evaluation attempt defined above. If, for example, $assertkill is executed in a timestep strictly after the last tick of the assertion clock for the evaluation attempt, then it shall not affect that attempt, even if $assertkill is executed no later than the next global clocking tick. Execution of the action block of an assertion containing global clocking future sampled value functions shall be delayed until the global clocking tick that follows the last tick of the assertion clock for the attempt. If the evaluation attempt fails and $error is called by default (see 16.14.1), then $error shall be called at the global clocking tick that follows the last tick of the assertion clock. A tool specific message that reports the starting or ending timestep of an evaluation attempt of an assertion containing global clocking future sampled functions shall be consistent with the definition above of the interval of simulation timesteps for the evaluation attempt. The message may also report the timestep in which it is written, which may be that of the global clocking tick that follows the last tick of the assertion clock. * After the preceding rewrite, I would remove the paragraph For assertions containing the behavior of the disable iff clause and other asynchronous assertion related controls (e.g. $assertkill, see 19.10) remains consistent with its behavior for assertions without global clocking future sampled value functions (see 16.12). that precedes Example 3. * Example 3. Change since rst was inactive between times 70 and 80 to since rst is inactive at time 80. The interval of the failing evaluation attempt starts and ends at time 80. Although rst is active prior to the execution of the action block at time 90, the attempt is not disabled. Also, remove the comma before "since". > Hi John, > > I am awfully sorry, but I didn't upload the correct version (now it is > in Mantis). > > I am talking about the text: > > " An evaluation attempt of an assertion containing global clocking > future sampled value functions ends at the global clocking tick that > follows the assertion clock tick at which the final boolean expression > of the assertion is evaluated. This allows the evaluation of the global > clocking future sampled value functions to be delayed until after the > next values of the referenced signals have been computed. Note however, > that the behavior of the disable iff clause and other asynchronous > assertion related controls (e.g. $assertkill, see 19.10) remains > consistent with its behavior for assertions without global clocking > future sampled value functions (see 16.12): the completion of the > property evaluation does not include (or is not contingent on) the > additional global clocking tick." > > on page 2 and Example 3 which follows it. > > Thanks, > Dmitry --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.
This archive was generated by hypermail 2.1.8 : Thu Dec 13 2007 - 06:53:37 PST