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

Hi Doron,

The motivation section in the preamble to this proposal contains an
example illustrating the efficiency issues.

Thanks,
Dmitry

-----Original Message-----
From: Bustan, Doron 
Sent: Sunday, September 16, 2007 9:24 AM
To: john.havlicek@freescale.com
Cc: piper@cadence.com; Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: RE: [sv-ac] reminder to vote on 1681

It looks like I misunderstood several things, so my reply is not so
relevant. You are right a parameter will not work, but I do think that
`define will, the idea in general was to use the global clock only in
the environment where the assertions clock is the only clock. 

I must say that I after reading Dmitry's explanations I don't understand
how the global clock can be used for performance optimizations in FV.

Doron 

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Wednesday, September 12, 2007 4:30 PM
To: Bustan, Doron
Cc: piper@cadence.com; Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: Re: [sv-ac] reminder to vote on 1681

Hi Doron:

I don't understand the details of your suggestion.

Are you saying that the assertions of BLK1 should be written in a 
module and that one of the parameters of the module should 
be aclk1?  In this case, I would want to be sure that it is
legal to set the parameter both to $global_clock and to 
"posedge clk1", e.g. in the bind directive.  It is not obvious
to me that setting a parameter in these ways is legal.

Otherwise, what are the specifics of the mechanism that you 
have in mind to switch between $global_clock and "posedge clk1"?
It would be helpful to write down a small amount of specific
code to illustrate the idea.

J.H.

> X-Authentication-Warning: server.eda-stds.org: majordom set sender to
owner-sv-ac@eda.org using -f
> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.20,242,1186383600"; 
>    d="scan'208";a="293111121"
> X-MIMEOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Wed, 12 Sep 2007 08:00:34 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] reminder to vote on 1681
> Thread-Index: Acf0anvr69ALGYkjSguXlrYq5OfjtgAVbB5gAA4XepA=
> From: "Bustan, Doron" <doron.bustan@intel.com>
> Cc: <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 12 Sep 2007 05:00:34.0897 (UTC)
FILETIME=[DA3F6410:01C7F4F9]
> X-eda.org-MailScanner: Found to be clean, Found to be clean
> X-Spam-Status: No, No
> X-MIME-Autoconverted: from quoted-printable to 8bit by
server.eda-stds.org id l8C51BM7016092
> Sender: owner-sv-ac@eda.org
> X-eda.org-MailScanner-Information: Please contact the ISP for more
information
> X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org
> 
> Hi Lisa,
> 
> I think that the problem that you describe can be solved using
> methodology.
> For example clock all the assertions of BLK1 on a parameter aclk1 that
> in the single block formal environment is set to $global_clock and in
> simulation to "posedge clk1".
> 
> However, I do not see a similar solution for next state functions. I
> think that by definition, you will not be able to reuse them in a
multi
> clock environment because you cannot expect the $rising function at
> block1 to use clk1 and the same function at block2 to use clk2.
> 
> As for the declaration of the global clock, I think that the easiest
> solution is to put it in it's own module and bind it to the top level
> module of the block.
> 
> Doron
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org]
On
> Behalf Of Lisa Piper
> Sent: Wednesday, September 12, 2007 5:00 AM
> To: Korchemny, Dmitry
> Cc: sv-ac@server.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
> 
> 
> 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
> 
> -- 
> 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.
> ---------------------------------------------------------------------
> 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.
> 
> 
---------------------------------------------------------------------
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.