RE: [sv-ac] Review of Mantis 1681 Proposal: Global clocking

Hi Tom,

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Thomas Thatcher
Sent: Thursday, July 12, 2007 2:14 AM
To: sv-ac@server.eda-stds.org
Subject: [sv-ac] Review of Mantis 1681 Proposal: Global clocking

Hello Everyone,

I have reviewed Mantis 1681.  Here are my comments.

1.  Should there be a mention of global clocking in clause 16.15?

    "There are a number of ways to specify a clock for a property:"
     Add  "-- Reference to $global_clocking when a global clock is
defined"

[Korchemny, Dmitry] My original intent was to infer the property clock
from the global clocking if it was not defined and could not be inferred
in another way. But in one of our last meetings we agreed that the clock
inference would not the global clocking into account. Therefore clause
16.15 need not be modified.

2.  I'm not sure about the clock rewrite rules.  It seems to me that if

	@(c) b  ---> (!c[*0:$] ##1 c & b)

    then the new re-write rule for global_clock should be:

      @($global_clock) b  ---> (!($global_clock)[*0:$] ##1 $global_clock
& b)

    But maybe my understanding of these rules is incorrect.  My
    interpretation is that an unclocked property is evaluated on every
    simulation time-step.  For the re-write rules, $global_clock is
going to
    act like any other clock.  The rule as Dmitry wrote it would only
hold if
    the number of simulation ticks was equal to the number of global
clock
    ticks.

[Korchemny, Dmitry] The main reason to introduce the global clock was to
be able to specify the reference clock of the system, i.e., the finest
granularity clock. @(c) b  ---> (!c[*0:$] ##1 c & b) reflects this
semantics. Only this definition allows introducing the next value
functions. The ideal situation would be to define the global clock as a
simulation tick in simulation. Unfortunately, doing this makes the
simulation very inefficient, and therefore it was suggested to pick some
clock to represent the reference clock in the simulation. It is assumed
that the global clock is the finest granularity clock for a given
assertion. The previous version did contain some synchronization
requirements to the assertion clocks, but it was suggested to remove
these requirements altogether because checking them exhaustively was
very costly. We can add a comment to the rewrite rule in question that
this is the intended semantics, but in simulation it is not guaranteed
by the language rules, and therefore in the simulation @($global_clock)
b  ---> (!($global_clock)[*0:$] ##1 $global_clock & b) has to be
implemented.

Tom
-- 
------------------
Thomas J. Thatcher
Sun Microsystems
408-616-5589
------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.