RE: [sv-ac] reminder to vote on 1681

Hi Tom,

As I mentioned in my reply to Lisa, there is no mapping of the system
clock for formal verification, but for simulation only.

When you simulate each block individually the definition of the global
clocking is straightforward. When you simulate them together, the
definition would be:

global clocking @(sysclk or ddr_clk or mac_tx_clk or mac_rx_clk);

Note, however that this definition should not have significant impact on
your simulation performance, since typically the fraction of the
assertions based on the global clock is small. The simulation
performance of assertions which do not explicitly use $global_clock is
not affected.

See my answer to Lisa about global clocking declaration in different
modules - it makes sense to declare them in the wrappers, and not in the
modules themselves. If you want to declare the global clocking in DUT
for some reason (though I would not recommend doing that), you need to
use compiler directives:

module dut;

`ifdef DUT_COMPILATION
	global clocking @(posedge clk); endclocking
`endif

Regards,
Dmitry

-----Original Message-----
From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] 
Sent: Wednesday, September 12, 2007 8:53 AM
To: Lisa Piper
Cc: Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: Re: [sv-ac] reminder to vote on 1681

Hello Everyone,

Let's make the example more concrete.  Suppose you are designing a CPU.

The CPU core will
run at, say 1.2 GHz (sysclk).  The core contains a DDR2 memory 
controller. The primary clock for
the DDR2 controller is 600 MHz (ddr_clk).  Also included is a 10G 
ethernet MAC, which is clocked
at 250 MHz (mac_tx_clk).  The receive side is clocked at 250.00001 MHz 
(mac_rx_clk). (no two
crystals are exactly the same).

What's really interesting is, if a global clock is used, how is it put 
in the code for formal verification
of each of the four small blocks.  Then how are all the blocks 
integrated so that system-level simulation can be
run?

Thanks,

Tom

Lisa Piper wrote:

>Hi Dmitry,
>
>I believe the 1681 proposal specifies the formal verification part
well,
>but I think clarification is needed on the use model. I think I
>understand it, but it was not clear from the writeup when to use
>references to $global_clock.
>
>For example, let's say I have 3 blocks and each has their own clock,
and
>I am going to use formal verification on each of Blk1, Blk2, and Blk3:
>
>	Blk1 defines the global clock to be @(posedge clk1)    
>	Blk2 defines the global clock to be @(posedge clk2)
>	Blk3 defines the global clock to be @(posedge clk3)
>
>Below shows two equivalent ways ("a" and "b") to create my code for
each
>block:
>
>Block 1 assertions:
>		global clocking @(posedge clk1); endclocking
>   a)	assert property ( @(posedge clk1)  x1 ##1 y1 |=> z1 );
>   b)	assert property ( @($global_clock) x1 ##1 y1 |=> z1 );
>
>Block 2 assertions:
>		global clocking @(posedge clk2); endclocking 
>   a)	assert property ( @(posedge clk2)  x2 ##1 y2 |=> z2 );
>   b)	assert property ( @($global_clock) x2 ##1 y2 |=> z2 );
>
>Block 3 assertions:
>		global clocking @(posedge clk3); endclocking
>   a)	assert property ( @(posedge clk3)  x3 ##1 y3 |=> z3 );
>   b)	assert property ( @($global_clock) x3 ##1 y3 |=> z3 );
>
>Both "a" and "b" work for formal verification and for simulation of
each
>block independently. However, when I integrate my 3 blocks into one
>elaborated snapshot, only approach "a" will work properly.
>
>In general, one should write all assertions that are sequential in
>nature using their appropriate design clk, not the global clock. It is
>only safe to use the global clock ($global_clock) for what could be
>modeled as an unclocked assertion where the frequency of the clock is
>irrelevant.
>
>A question - if I were going to do formal analysis on all 3 blocks,
>would I define the global clock as:
>
>	global clocking @(posedge clk1 or posedge clk2 or posedge clk3);
>endclocking
>
>
>A second thing that concerns me is that this global clocking is
>specified in a clocking block, which is typically in a testbench, and
>not in the modules that would go to the formal tool. Is the use model
to
>define one clocking block for simulation and a different one for
formal?
>And if this is the case, why not just do it outside the clocking block
>similar to the way `timescale is defined.
>
>Lisa
>
>-----Original Message-----
>From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
John
>Havlicek
>Sent: Tuesday, September 11, 2007 7:54 AM
>To: sv-ac@eda-stds.org
>Subject: [sv-ac] reminder to vote on 1681
>
>Hi Folks:
>
>This is a reminder that we have a ballot on 1681 
>closing at 2007-09-13 T 23:59-07:00(PDT).
>
>Below are the results so far.
>
>Please vote if you are eligible.
>
>J.H.
>
>-----------------------------------------------------------------------
-
>------
>
>Ballot on Mantis 1681
>
>- Called on 2007-09-06, final ballots due by 2007-09-13 T
>23:59-07:00(PDT).
>
>yv[xxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel)
>yv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)     
> n[------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys)
>yv[xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale)
> t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair)
>yv[xxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel -
>Co-Chair)
> v[xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor
>Graphics)
> n[--------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics)
> n[------x--xxx.....................] Joseph Lu (Altera)
> v[xxx..............................] Johan Martensson (Jasper)
> n[-----------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale)
> v[xxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
>yv[xxxxx-x-xxxxx-x..................] Erik Seligman (Intel)
> n[-------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics)
> v[-xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys)
> v[xxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems)
>   |--------------------------------- attendance on 2007-09-04
> |----------------------------------- voting eligibility for this
ballot
>|------------------------------------ email ballots received
>
>
>
>	Legend:
>		x = attended
>		- = missed
>		r = represented
>		. = not yet a member
>		v = valid voter (2 out of last 3 or 3/4 overall)
>		n = not valid voter
>                t = chair eligible to vote only to make or break a tie
>
>  
>
---------------------------------------------------------------------
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.