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.