[sv-ac] suggestions for 1682

From: John Havlicek <john.havlicek_at_.....>
Date: Wed Dec 12 2007 - 10:53:12 PST
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

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Wed Dec 12 11:33:02 2007

This archive was generated by hypermail 2.1.8 : Wed Dec 12 2007 - 11:33:47 PST