Hi, I think the informal semantics of chapter 16 of the LRM is very simulation centric in certain places and a semantics for the context of formal verification is more or less unspecified there. A case in point is 16.14.3. I don't think the text there makes much sense in the context of formal verification. A semantics for cover of sequences could well be given for formal, I think. I'm not so sure about cover of properties in general though. Best Regards, Johan M On Thu, Aug 30, 2007 at 06:20:39PM +0300, Bresticker, Shalom wrote: > 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. > > -- ------------------------------------------------------------ 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 Thu Aug 30 08:55:28 2007
This archive was generated by hypermail 2.1.8 : Thu Aug 30 2007 - 08:55:40 PDT