RE: [sv-ac] Re: [sv-ec] mantis item 1681 - global clocking

<forwarding bounced email from Korchemny, Dmitry>

-------- Original Message --------
Subject: RE: [sv-ac] Re: [sv-ec] mantis item 1681 - global clocking
Date: Fri, 02 Mar 2007 05:44:06 +0200
From: Korchemny, Dmitry <dmitry.korchemny@intel.com>
To: Neil.Korpusik@Sun.COM, SV_EC List <sv-ec@eda.org>, sv-ac@eda-stds.org
CC: adam.krolnik@verisilicon.com

Hi Mr. Krolnik,

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 Neil Korpusik
Sent: Wednesday, February 28, 2007 8:12 PM
To: SV_EC List; sv-ac@server.eda-stds.org
Cc: adam.krolnik@verisilicon.com
Subject: [sv-ac] Re: [sv-ec] mantis item 1681 - global clocking

<forwarding email from Adam Krolnik>

-------- Original Message --------
Date: Wed, 28 Feb 2007 08:48:44 -0600
From: Adam Krolnik <adam.krolnik@verisilicon.com>
To: SV_EC List <sv-ec@server.eda.org>
CC: Havlicek John <john.havlicek@freescale.com>, Sv_Ac
<sv-ac@server.eda.org>
Subject: Re: [sv-ec] mantis item 1681 - global clocking

Good morning all;

The idea of a global clock is interesting, but seems to be a problematic
for reuse.

The spec says in 15.12 "The main purpose of the global clock[ing] is to
introduce the [a] common system clock
for all concurrent assertions in the entire design. This is convenient
for synchronous designs."

What about synchronous designs with multiple clock domains. Surely, one
would agree that a design
with a JTAG controller (that has its clock) and main logic (with its own
clock) is still a synchronous system.
Yet clocking assertions from these two domains with one clock will
produce possibly wrong results compared
with clocking assertions with the local domain clock.

An example is shown:

   ...
   global clocking sys @(clk1 or clk2); endclocking

This example will need some explaining. Why is the global clock the
combination of all events of clk1 + clk2?
It is not common to see designs clocked on both edges of a clock.
Assertions written for one clock domain
will definitely fail if clocked with this global clock that has 4 times
the number of events as the logic.

[Korchemny, Dmitry] If your assertion is written relative to some clock
domain, it will behave absolutely the same way with global clocking and
without it. Therefore the correctness will not be broken.

E.g.,
clocking sys @(clk1 or clk2); endclocking

does not affect the assertion

assert property (@(posedge clk1) a);

In 17.3, it states, "where global clocking has been specified ... for
correct operation the user should make sure that
the ticks of all other clocks are aligned with the ticks of the global
clock. The simulation tool may issue an error message when it detects
that this requirement has been violated."

How can one fulfill this requirement in the general case simulation. I
have designs that have 3-4 clock domains, running
at different frequencies (some synchronous to each other, some not.) I'm
sure larger companies have dozens of clock domains.

[Korchemny, Dmitry] This requirement may be relaxed for assertions that
can be written according to the current LRM. It is gating for new
enhancements to be introduced (e.g., next value functions).

Also, having global clocking is (and was) important to keep  formal
verification of multiclock synchronous designs consistent with their
simulation. Thus, if you have two clocks clk1 and clk2 in your design,
the formal verification tool will  normally require a clock pattern,
e.g., clk1 has a pattern 0011, and clk2 01110. This is equivalent to the
global clock introduction.

The example in 17.14 shows this point. The property

    property p5;
       (a |-> ##2 b);
    endproperty

Is supposed to expect that B ocurrs 2 cycles after A. If you combine
that with the global clocking specification above,
how can this property be expected to pass when simulated with 4 edges of
a clock counting as a 'cycle'.

[Korchemny, Dmitry] The inference of the global clock will occur if no
clock can be inferred otherwise. If, say, you write:

always (@(posedge clk2)) assert property(p5);

the clock of p5 will be posedge clk2, and not the global clock.

Instead of a global clock block, it would be more useful to have a
hierarchical default clock. Assertions obtain their
clock from the current scope, or the parent scope, up to this
hierarchical default clock. That way a verification engineer
can specify a clock block for a clock domain and place the required
clock block at the necessary levels of hierarchy to achieve this. Most
likely this would be something that is bound (via the bind statement) to
modules in a design.

With this approach, one can define the default clock for each domain
however the system is composed of pieces and
their specific clock domain.

[Korchemny, Dmitry] You are welcome to submit this enhancement.
-- 
    Soli Deo Gloria
    Adam Krolnik
    Director of Design Verification
    VeriSilicon Inc.
    Plano TX. 75074
    Co-author "Assertion-Based Design"







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