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

Hi Lisa,

The global clock is not intended to substitute the usage of the regular
clock - whenever the regular clock is needed, it is incorrect to use a
global clock instead. In your examples 

		global clocking @(posedge clk1); endclocking
   a)	assert property ( @(posedge clk1)  x1 ##1 y1 |=> z1 );
   b)	assert property ( @($global_clock) x1 ##1 y1 |=> z1 );

assertions a) and b) have DIFFERENT meaning in simulation and in FV (I
would not use the assertion b) for FV, except for the case when there is
a single clocked system).

For FV the assertion b) means that WHATEVER your clock is, when there
are x1 followed by y1 they must be followed by z1 according to the ticks
of an ARBITRARY clock. In the simulation assertions a) and b) coincide.

We also should distinguish between the global clocking and global clock
- in FV there is no need in global clocking, but just in $global_clock,
and there is no mapping of the global clock in FV - it corresponds to 1
(see Annex E changes in this proposal). The fact that the global
clocking defines that posedge clk1 is a global clock is ignored in FV.
But to be able to run an assertion in simulation you need to map your
reference clock to the real event, and it what the global clocking is
used for.

Now, about the intended usage of the global clock: the global clock
should be used in properties when the property must remain valid for any
clock. One of such cases that you mentioned, are so called "unclocked"
property. E.g., two outputs of a circuit are ALWAYS identical, whatever
the system clock is. If I write my assertion as:

assert property (@(posedge clk) a == b);

and then introduce a faster clock into the system, this assertion is not
sufficient anymore. In this case the correct way to write it is:

assert property (@$global_clock a == b);

Another important class is stability assertions, e.g., that a signal is
stable between two consecutive clock ticks, and this kind of assertion
is very common in practice.

The robust way to write this property is:

property stable_between_ticks(sig, clk);
    @$global_clock disable iff(rst)
        $rose(clk) ##1 (!$rose(clk)[*1:$]) |-> ($past(sig) ==
$past(sig,2));
endproperty : stable_between_ticks

(or even more efficient for FV using temporal operators:

@$global_clock clk |-> ($steady_gclk(sig) until $rising_gclk(clk))

There may be several interpretations of the above English statement,
this is one of them)

Another example of a property : the property saying the a clock is
ticking:

(always) @($global_clock) ##[0:$] $changed(clk);

Or FV-friendlier version

(always) @($global_clock) ##[0:$] $changing_gclk(clk);

I hope that the above examples illustrate the usage and the importance
of the global clock.

See my other comments below.

Thanks,
Dmitry
 
-----Original Message-----
From: Lisa Piper [mailto:piper@cadence.com] 
Sent: Wednesday, September 12, 2007 5:00 AM
To: Korchemny, Dmitry
Cc: sv-ac@eda-stds.org
Subject: RE: [sv-ac] reminder to vote on 1681

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

[Korchemny, Dmitry] I would not use global clock in either of these
assertions (see the preamble). Also, as I mentioned global clock mapping
is not intended for formal. As for the simulation, I agree with your
definition - it is OR of all the clocking events.


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?

[Korchemny, Dmitry] Again, formal does not use this clocking block at
all (see the preamble).

And if this is the case, why not just do it outside the clocking block
similar to the way `timescale is defined.

[Korchemny, Dmitry] The global clocking using our current definition has
to be specified in one of the modules, typically in the top module.

Assume that you have three modules, Blk1, Blk2, and Blk3. Usually there
are top modules, containing your DUT and instantiating the test bench.
It makes sense to put the global clocking definition there.

E.g.,

module Sys1 // Wrapper for Blk1
	global clocking @(posedge clk1); endclocking
	
	Blk1 b1(i1, o1);
	...
endmodule

module Sys // Wrapper for three modules Blk1, Blk2, Blk3
	global clocking @(posedge clk1 or posedge clk2 or posedge clk3);
	endclocking
	...
	Blk1 b1(i1, o1);
	Blk2 b2(o1, o2);
	Blk3 b3(o2, o3);
	...

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

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
---------------------------------------------------------------------
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.