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.
> 
> 

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