Thanks Dmitry, I understand now. I missed the fact that the global clocking declaration will primarily be used for simulation to give a semantics to $global_clock and the $<something>_gclk() system functions in that context. A couple of questions: a) It seems that a global clocking declaration is not really necessary in order to give a meaning to $global_clock and $<something>_gclk() in FV. Is that right? Nevertheless it is stated in 14.13 that "It shall be an error to invoke the $global_clock system function if there is no global clocking declaration in the elaborated SystemVerilog model." Is the intent that this would be obligatory for FV also. b) If there is a global clocking declaration, is the intention that this declaration will influence the way a transition system is derived from the DUV in FV? E.g. will this declaration define the finest granularity of the analysis? Best Regards, Johan On Wed, Sep 12, 2007 at 05:11:15PM +0300, Korchemny, Dmitry wrote: > Hi Johan, > > I hope that my reply to Lisa addresses your concerns. We are talking about different usage models. > > Regards, > Dmitry > > -----Original Message----- > From: johan.martensson@jasper-da.com [mailto:johan.martensson@jasper-da.com] > Sent: Wednesday, September 12, 2007 12:35 PM > To: Bustan, Doron; Korchemny, Dmitry > Cc: Lisa Piper; sv-ac@eda-stds.org > Subject: Re: [sv-ac] reminder to vote on 1681 > > Hi Dmitry and Doron, > > I think for formal verification a more flexible and expressive framework > may be called for than what is proposed in 1681. > > I agree there should be a way to tell the tool what signal is the > fastest clock, but I think it would also be useful to be able to specify > other signals as additional clocks with a fixed frequency and phase > relation to the fastest one (the global clock). > > I'm not sure wheter this is best specified in the input files or when > setting up the verification environment in the formal tool. The second > alternative seems more flexible. To illustrate this using Lisa's example > below: > > i) When for example Blk1 is verified separately clk1 is specified as the > fastest clock. > > ii) When all three blocks are integrated, (and clk1, clk2 and clk3 are > connected to csig1, csig2 and csig3) then for example csig2 is specified > as the fastest clock, csig1 as having frequency 1/2 and phase shift 1 > (w.r.t. to the fastest clock) and csig3 as having frequency 1/3 and phase > shift 2. > > All this information would be useful to a formal tool and I think > specifying it in the SV input files might be a bit cumbersome given the > need to shift the focus of verification from a single module to the > environment in which it is instantiated for example, and so possibly > having to edit the input files. > > Now (as Doron did point out) changing the fastest clock (global clock) > for different verification passes would change the semantics for the > $<something>_gclk() system functions proposed in mantis 1682. > > A remedy for this would perhaps be to require a second argument to these > functions specifying the respective clock expression. And then issue an > error if the frequency and phase w.r.t. the fastest clock is not > defined. > > Best Regards, > > Johan M > > On Wed, Sep 12, 2007 at 08:00:34AM +0300, Bustan, Doron wrote: > > 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. > > > > > > -- > ------------------------------------------------------------ > Johan Mårtensson Office: +46 31 7451913 > Jasper Design Automation Mobile: +46 703749681 > Arvid Hedvalls backe 4 Fax: +46 31 7451939 > 411 33 Gothenburg, Sweden Skype ID: johanmartensson > ------------------------------------------------------------ > --------------------------------------------------------------------- > 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. -- ------------------------------------------------------------ Johan Mårtensson Office: +46 31 7451913 Jasper Design Automation Mobile: +46 703749681 Arvid Hedvalls backe 4 Fax: +46 31 7451939 411 33 Gothenburg, Sweden Skype ID: johanmartensson ------------------------------------------------------------ -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Wed Sep 12 08:28:12 2007
This archive was generated by hypermail 2.1.8 : Wed Sep 12 2007 - 08:28:27 PDT