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.