Hi Shalom, Arturo, There are two points here. One is what the global clocking is concerned, and the other is about the language focus. The main purpose of introducing the global clocking was simulation, and even more precisely, even-driven simulation, since the global clocking binds a reference clock to a simulation event. For formal verification and cycle-based simulation the global clocking construct is not needed, $global_clock is defined in the natural way in their context. As for the focus of the language is concerned, though simulation is its primary focus without any doubt, limiting the language to simulation constructs only is not sufficient for formal verification, and there are several reasons for it: 1. In simulation we deal with finite traces only, and in formal verification we deal with infinite traces, 2. In simulation only one input trace is considered, while in formal verification the set of all feasible traces are dealt at once. 3. Another issue is that the formal verification of RTL is synchronous by its nature, while the simulation time is virtually continuous. All these issues need to be addressed in the language in order to be able to support formal verification, Many of them have already been addressed in Annex F (Formal semantics of concurrent assertions). Thanks, Dmitry ________________________________ From: Bresticker, Shalom Sent: Friday, August 31, 2007 5:49 PM To: Arturo Salz; Korchemny, Dmitry; john.havlicek@freescale.com Cc: sv-ac@eda-stds.org Subject: RE: [sv-ac] 1691 Introduce global clocking If you read those passages carefully, they do not say that the existence of constructs in the language is driven primary by simulation, but rather that their semantics is/are defined for simulation. So it is for global clocking also. The proposal describes its semantics primarily in terms of simulation. I think. Shalom ________________________________ From: Arturo Salz [mailto:Arturo.Salz@synopsys.com] Sent: Thursday, August 30, 2007 9:55 PM To: Bresticker, Shalom; Korchemny, Dmitry; john.havlicek@freescale.com Cc: sv-ac@eda-stds.org Subject: RE: [sv-ac] 1691 Introduce global clocking Shalom's statement is supported by the Verilog and SystemVerilog LRM's. Note that it doesn't say that semantics other than simulation are unimportant, but that the (primary) semantics of the language are defined for simulation. IEEE 1364-2205 (page 158) Although the Verilog HDL is used for more than simulation, the semantics of the language are defined for simulation, and everything else is abstracted from this base definition. IEEE 1800-2005 (page 120) NOTE-This clause gives an overview of the interactions between these elements, especially with respect to the scheduling and execution of events. Although SystemVerilog is not limited to simulation, the semantics of the language is defined for event-directed simulation, and other uses of the HDL are abstracted from this base definition. Arturo -----Original Message----- From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Bresticker, Shalom Sent: Thursday, August 30, 2007 8:21 AM To: Korchemny, Dmitry; john.havlicek@freescale.com Cc: sv-ac@eda-stds.org Subject: RE: [sv-ac] 1691 Introduce global clocking That is what you have to convince others, because not everyone shares your opinion today. It is not self-evident to everyone. Shalom > -----Original Message----- > From: Korchemny, Dmitry > Sent: Thursday, August 30, 2007 4:52 PM > To: Bresticker, Shalom; 'john.havlicek@freescale.com' > Cc: 'sv-ac@server.eda-stds.org' > Subject: RE: [sv-ac] 1691 Introduce global clocking > > Hi Shalom, > > I also agree with John's comments, but I cannot agree that SV > is a simulation language only and that the other aspects are > not important. E.g., in the context of simulation you cannot > talk about such basic formal verification concepts as > fairness and liveness. If we are going to limit ourselves to > simulation aspects only then the right solution would be to > replace SVA with PSL, and let each language do its own job. > > I think that the advantage of SVA is in its native > integration with the rest of SV, and if we want to keep SVA > as part of the language we need to change our perception of > SV as a simulation language only. > > Thanks, > Dmitry > > -----Original Message----- > From: Bresticker, Shalom > Sent: Wednesday, August 29, 2007 10:50 AM > To: john.havlicek@freescale.com; Korchemny, Dmitry > Cc: sv-ac@server.eda-stds.org > Subject: RE: [sv-ac] 1691 Introduce global clocking > > I like John's suggestions. > > FYI, I participated in the champions' discussion on this > issue. I believe the biggest single reservation the > participants had was about the justification for a > non-simulation construct, in the same way that the LRM does > not have special constructs for synthesis. SystemVerilog is > first and foremost a simulation language. All the semantics > are defined in this context. > > So the justification for adding a construct driven by formal > verification needs has to be strong on this point. > > One might ask, for example, why not use attributes, which > were introduced as a way of allowing non-simulation > characteristics in the hardware description, while being > ignored by simulation? In your case, however, you want to > write assertions, which are part of the simulation language, > using the global clock. > > Regards, > Shalom > > > > -----Original Message----- > > From: owner-sv-ac@server.eda.org > > [mailto:owner-sv-ac@server.eda.org] On Behalf Of John Havlicek > > Sent: Wednesday, August 29, 2007 5:40 AM > > To: Korchemny, Dmitry > > Cc: sv-ac@server.eda-stds.org > > Subject: Re: [sv-ac] 1691 Introduce global clocking > > > > Hi Dmitry: > > > > I have a few suggestions below. Feel free to follow them or not. > > > > J.H. > > > > . I recommend adjusting > > > > The global clocking is not directly related to the compilation > > units. > > The requirement is to be at most one global clocking statement > > after the > > elaboration stage. > > > > to > > > > Global clocking is not directly related to compilation units. > > The requirement is that there be at most one global clocking > > statement after the elaboration stage. The global clocking > > statement applies to the entire elaborated model, regardless of > > the particular compilation unit in which it appears. > > > > . I recommend adjusting > > > > * The LRM is based on event based simulation. > > > > This is exactly the reason why the global clocking is needed. > > There is > > no need in a concept of global clocking for cycle-based > > simulation - the > > notion of the reference clock is already in the > language in this > > case. > > > > to > > > > * The LRM is based on event based simulation. > > > > SystemVerilog provides a unified language for writing > both design > > models and associated assertion-based specifications. > These are > > used not only in simulation, but also in formal verification, > > where the tractability of the verification computation usually > > hinges on abstraction and simplification of the event-based > > semantics. The purpose of the global clocking construct is to > > provide a way to specify the primary clock that synchronizes > > transitions in formal models and thereby obtain efficiencies in > > formal verification computations. > > > > . I recommend adjusting > > > > * If in a package would need to be imported > > > > Global clocking cannot be specified in a package. > > > > to > > > > * If in a package would need to be imported > > > > Global clocking cannot be specified in a package. Global > > clocking may be referenced by items declared within a package. > > > > . I recomment adjusting > > > > * Not sure why need this global thing, we already have > clocking > > blocks. > > > > Using clocking events defined by regular clocking blocks is not > > different from the assertion point of view from the regular > > clocking > > events. Using default clocking does not solve the problem, > > either, > > because default clocking definition may differ from module to > > module. We > > need to specify the same clock for all assertions that > reference > > it > > explicitly, to be able to explicitly specify a transition > > relation. > > > > to > > > > * Not sure why need this global thing, we already have > clocking > > blocks. > > > > The purpose of the global clocking construct is to > provide a way > > to specify the primary clock that synchronizes transitions in > > formal models and thereby obtain efficiencies in formal > > verification computations. Using clocking events defined by > > regular clocking blocks, even the default for a > particular scope, > > does not accomplish specification of the global > primary clock for > > the entire formal model. > > > > > 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.19,317,1183359600"; > > > d="scan'208,217";a="289422246" > > > X-MimeOLE: Produced By Microsoft Exchange V6.5 > > > Content-class: urn:content-classes:message > > > Date: Tue, 28 Aug 2007 18:27:48 +0300 > > > X-MS-Has-Attach: > > > X-MS-TNEF-Correlator: > > > Thread-Topic: [sv-ac] 1691 Introduce global clocking > > > Thread-Index: Acfph/1CV4O2OzAsRDSQLPsipsiQ9A== > > > From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com> > > > X-OriginalArrivalTime: 28 Aug 2007 15:27:57.0196 (UTC) > > > FILETIME=[029C24C0:01C7E988] > > > X-eda.org-MailScanner: Found to be clean, Found to be clean > > > X-Spam-Status: No, No > > > 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 > > > > > > This is a multi-part message in MIME format. > > > > > > ------_=_NextPart_001_01C7E987.FD5B7206 > > > Content-Type: text/plain; > > > charset="us-ascii" > > > Content-Transfer-Encoding: quoted-printable > > > > > > Hi all, > > > > > > =20 > > > > > > I had an action item to address the champions' comments concerning > > > 1691 "Introduce global clocking". Please, find below my > answer for > > > your review. > > > > > > =20 > > > > > > Thanks, > > > > > > Dmitry > > > > > > =20 > > > > > > * The proposal doesn't discuss what the global clock is with > > > respect to compilation units=20 > > > > > > =20 > > > > > > The global clocking is not directly related to the > > compilation units. > > > The requirement is to be at most one global clocking > > statement after > > > the elaboration stage. > > > > > > =20 > > > > > > * There is no concept of globals in SystemVerilog=20 > > > > > > =20 > > > > > > The concept of globals is mentioned in the LRM. See for > > example Clause > > > 3.12.3 "Simulation time unit". It states: > > > > > > =20 > > > > > > "The global time precision, also called the simulation time > > unit, is > > > the minimum of all the timeprecision statements and the > > smallest time > > > precision argument of all the `timescale compiler > directives in the > > > design. The step time unit is equal to the global time precision." > > > > > > =20 > > > > > > There is also a notion of a global symbol/task/function in > > Clause 34. > > > > > > =20 > > > > > > * It should be a tool option=20 > > > > > > =20 > > > > > > This seems to be problematic since a transition to a new > > tool becomes > > > unpredictable. We should take advantage of standardizing > > it, to make > > > this concept well-defined. > > > > > > =20 > > > > > > * Strange that it is global and needs to be in a module, it should > > > be in compilation unit space=20 > > > > > > =20 > > > > > > Since the global clocking defines a clocking event, it > > makes sense to > > > consider it as a kind of clocking, and not as an absolutely new > > > construct. LRM defines that the clocking block shall not > > appear in a > > > compilation unit space, this is why the global clocking > declaration > > > rules have been defined in a similar way. The consistency > > is crucial > > > here. > > > > > > =20 > > > > > > * Not sure it fits in with the general usage of the language=20 > > > > > > =20 > > > > > > In the introduction to the LRM it is written: > > > > > > "SystemVerilog enables the use of a unified language for > > abstract and > > > detailed specification of the design, specification of > assertions, > > > coverage, and testbench verification that is based on manual or > > > automatic methodologies."=20 > > > > > > =20 > > > > > > This implies that SystemVerilog should answer the needs of > > > assertion-based formal verification. For formal verification of > > > synchronous systems the notion of the reference clock is > important, > > > especially for multiclock design and for building abstract formal > > > models of the system. The detailed description of the > motivation of > > > this feature may be found in the preamble to 1681. > > > > > > =20 > > > > > > Since formal verification of RTL is in scope of the language, the > > > notion of the reference clock needs to be covered by the language. > > > > > > =20 > > > > > > * The LRM is based on event based simulation.=20 > > > > > > =20 > > > > > > This is exactly the reason why the global clocking is > > needed. There is > > > no need in a concept of global clocking for cycle-based > > simulation - > > > the notion of the reference clock is already in the > > language in this case. > > > > > > =20 > > > > > > * If in a package would need to be imported=20 > > > > > > =20 > > > > > > Global clocking cannot be specified in a package. > > > > > > =20 > > > > > > * Not sure why need this global thing, we already have clocking > > > blocks.=20 > > > > > > =20 > > > > > > Using clocking events defined by regular clocking blocks is not > > > different from the assertion point of view from the regular > > clocking > > > events. Using default clocking does not solve the > problem, either, > > > because default clocking definition may differ from module > > to module. > > > We need to specify the same clock for all assertions that > > reference it > > > explicitly, to be able to explicitly specify a transition > relation. > > > > > > =20 > > > > > > * The proposal says that global clock is for the design. Can the > > > testbench use the global clock? (proposal seems to not say)=20 > > > > > > =20 > > > > > > Yes, the test bench is also part of the design. The > global clocking > > > just defines an event which may be used everywhere. It does > > not differ > > > from any other event except for the formal semantics of > assertions > > > where it is considered to represent the reference clock. > > > > > > =20 > > > > > > * Proposal shouldn't use the term design if it isn't clear=20 > > > > > > =20 > > > > > > Unfortunately, there is no term in the LRM for the "whole > > thing" other > > > than design. The term "design" is already used in the LRM: > > > > > > =20 > > > > > > "The global time precision, also called the simulation time > > unit, is > > > the minimum of all the timeprecision statements and the > > smallest time > > > precision argument of all the `timescale compiler > directives in the > > > design. The step time unit is equal to the global time precision." > > > > > > =20 > > > > > > (again citing 3.12.3). > > > > > > =20 > > > > > > It seems reasonable to define a special term in the LRM > > specifying the > > > "whole thing", and then update 1681 proposal accordingly. > > We believe > > > that such basic terms should be introduced by SV-BC. > > > > > > =20 > > > > > > =20 > > > > -- > > 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. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Tue Sep 4 01:08:51 2007
This archive was generated by hypermail 2.1.8 : Tue Sep 04 2007 - 01:08:58 PDT