Hi Dimitry, I regard annex F as agnostic between simulation and formal verification. It gives a relation (of satisfaction) between a run and a formula. A relation of this sort is a prerequisite for defining both when a simulation tool should report an error for a formula on a run and when a formal tool should report validity or counterexample for example. What seems missing from the formal semantics in annex F is a definition of the semantics for the different concurrent assertion statements. It seems a semantics for the concurrent assertion statements would have to be given differenty for the case of simulation and formal verification respectively. For example for assert_property_statement in simulation the problem is to relate a concrete run and a property so the relation from Annex F seems to be more or less directly applicable, whereas in formal we need to say something about how the formula should relate to the members in the set of possible runs of the system. It seems an exact formal verification semantics can and should be given to assume_property_statement in relation to assert_property_statement in terms of the set of runs of a system, whereas for simulation maybe an exact semantics is not really feasible and/or desirable. Currently I don't think there is a great risk of confusion as to the formal verification semantics for asserts and assumes since I guess it is more or less straightforward how it should be formulated. In the case of cover_property_statement the case is not so clear I think. One intuition is to have the tool search for a trace where the property is exemplified. This may be pretty straigtforward in case the property is a simple sequence: simply find a (finite) trace where the sequence matches at least once. But what is desirable for properties in general? 1) Implication/Vacuity For example 'cover property r|=> s' for some sequences r and s. In this case any trace where the sequence r doesn't match is a witness for the property. Is it enough to present such a trace or should the tool look for a more interesting trace, a trace where r ##1 s matches, for example? 2) Infinite match In case the sequence is weakly embedded (mantis 1932) for example 'cover property a[*0:$] ##1 b' for a design where b can never happen but where there are infinite runs where a is true from some point onward. Should the tool present an looping trace in this case. 3) Liveness Are there some special considerations w.r.t. cover of liveness properties? For a formal tools company supporting SVA you are under pressure from customers to support as many constructs as possible from the LRM (and/or which they have been using for simulation). Now when an official semantics is lacking the temptation is to provide some idiosyncratic semantics that will then maybe not be forwards compatible and/or compatible with what happens in other tools. With mantis 1768 we get a cover_sequence_statement. I would be happy if we could give a well defined formal verification semantics for it and then maybe state that for cover_property_statement the formal verification semantics is not defined. Best Regards, Johan M On Tue, Sep 04, 2007 at 12:03:44PM +0300, Korchemny, Dmitry wrote: > Hi Johan, > > Though Clause 16 is in some sense simulation centric, Annex F is not. > I agree with you about cover statement, and we had several discussions > about it in the past, but haven't made any decision yet. The idea was > to define the cover statement as E<formula>, instead of A<formula> as > in case of assertions (E = existential quantification, and A = > universal quantification) for formal verification and to use it to > find a property witness. > > Note, however, that coverage is widely used in simulation, and > therefore it should be well elaborated for simulation as well. > > Thanks, Dmitry > > -----Original Message----- From: johan.martensson@jasper-da.com > [mailto:johan.martensson@jasper-da.com] Sent: Thursday, August 30, > 2007 6:55 PM To: sv-ac@eda-stds.org Cc: Korchemny, Dmitry; > john.havlicek@freescale.com; Bresticker, Shalom Subject: 16.14.3 and > simulation centric semantics. > > 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 > ------------------------------------------------------------ -- ------------------------------------------------------------ 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 Tue Sep 4 05:51:36 2007
This archive was generated by hypermail 2.1.8 : Tue Sep 04 2007 - 05:52:07 PDT