Subject: RE: [vhdl-200x] RE: Advisory vote: simple subset of PSL
From: Erich Marschner (erichm@cadence.com)
Date: Fri Sep 12 2003 - 15:33:49 PDT
Tom,
I would like to add a few points regarding the issues you have raised. (I'm speaking here as an individual participant in the VHDL 200x WG, not in my role as co-chair of the FVTC. The following remarks represent my personal opinion only and should not be taken as an official position of Accellera.)
First, regarding the stability of PSL, and for that matter, System Verilog Assertions (SVA):
In the July meeting in which the incorporation of PSL by reference into VHDL 200x was explored, I explained that PSL v1.01 is the current version of the standard, and that PSL v1.1 is now under development. I also explained that the focus of the PSL v1.1 effort is to achieve alignment between SVA and PSL. The committee was aware that PSL is evolving, just as System Verilog is continuing to evolve. In fact, Dennis Brophy's suggestion to incorporate PSL by reference, rather than by other means, was seen as a way of implicitly adapting to and benefiting from the enhancements that will become available in PSL v1.1. So I think the committee is well aware of this.
Also, it should be noted that both SVA and PSL have been changing as part of this alignment process. In working out the formal semantic mapping between the two languages, a number of issues - some mistakes, some intentional - have been identified in the formal semantics of both languages, and as a result some semantic changes have been proposed for both languages. The FVTC Alignment subcommittee overlaps with the System Verilog Assertions Committee, and a number of key people are common to both committees. Those key people (e.g., John Havlicek, Surrendra Dudani) have submitted SVA change proposals to the SV-AC that have come from the work done in the FVTC Alignment committee. As a result, both languages are evolving towards each other. I think everyone agrees that this is a good thing.
Second, regarding the adoption of a "reduced subset" of capabilities common to VHDL/Verilog/SystemVerilog:
I couldn't agree with you more. I believe that a well-defined assertion language that can work with various implementation languages (Verilog, SystemVerilog, VHDL, SystemC, etc.) can enable us to move towards formal specifications that are independent of the languages used to describe an implementation. This has been one of the goals of PSL. PSL is defined in 'flavors' for Verilog, VHDL, and GDL (previously EDL, an internal IBM language). (The VHDL 'flavor' of PSL is what the VHDL 200x committee is considering.) Each flavor is syntactically adapted to the underlying HDL, but at the same time uses a common set of temporal operators and verification directives, so there is commonality across the different HDLs it supports. The current work to align PSL and SVA is in effect defining a SystemVerilog 'flavor' of PSL, so that SystemVerilog will be supported at the same level as the other languages PSL currently supports. But the key characteristic of PSL is its ability to span multiple languages and provide
a common notation for assertions that work in all of them.
Also, regarding a "reduced subset" - as you know, PSL is fairly comprehensive, yet at the same time the PSL LRM defines various nested subsets of capability. In particular, the PSL LRM defines the Simple Subset, which consists of properties in which time moves monotonically left-to-right, which makes such properties easy to implement in both simulation and formal verification tools. It should be noted that it is the Simple Subset of PSL that the VHDL 200x assertions committee is considering. It should also be noted that the current work on SVA (in SystemVerilog 3.1a) seems to be expanding it to include more of the capabilities that are part of PSL's Simple Subset (e.g., nested properties). So the goal of having a common "reduced subset" of capabilities is being achieved.
Finally, regarding scheduling semantics:
I agree with you that it is important to implement carefully the scheduling of assertions in simulation in order to get consistent answers in simulation and in formal verification. This can be done without too much difficulty. To define the scheduling of assertions so that the same results are produced in VHDL and Verilog/SystemVerilog simulation is potentially more challenging, since the simulation cycle definitions are quite different among those three languages. The interaction between VHDL and Verilog simulation cycles has been fairly well understood for a number of years, but I'm not aware that anyone has yet proposed a way to interleave VHDL and SystemVerilog simulation cycles. (If you know of any such proposals, perhaps you could post them?) I think this may be a prerequisite before we can address the larger issue you've proposed.
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
| -----Original Message-----
| From: Tom Fitzpatrick [mailto:Tom.Fitzpatrick@synopsys.com]
| Sent: Friday, September 12, 2003 2:00 PM
| To: Bailey, Stephen; 'Tom Fitzpatrick'
| Cc: vhdl-200x@eda.org
| Subject: RE: [vhdl-200x] RE: Advisory vote: simple subset of PSL
|
|
| Hi Stephen,
|
| Thanks for your response, and for adding me to the reflector.
|
| I appreciate the difference between "cut-and-pasting" the PSL LRM and
| incorporating it by reference. As you point out, PSL1.01 is an Accellera
| standard and can be used in this context, I believe. Since Accellera has
| decided to move PSL to 1.1 to be compatible with SystemVerilog, and will, I
| imagine, encourage vendors and users to move along with them, I encourage
| VHDL-200x to be flexible on this point. I'd also encourage you to remind
| your audience of this fact whenever appropriate.
|
| As a representative of a vendor, I think there is a lot of value in reducing
| the number of languages that need to be supported. If we can agree on a
| "reduced subset" of assertion capability that is consistent between
| VHDL-200x and SystemVerilog/Verilog-200x, then everyone will benefit. I
| believe that the VHDL-200x committee is actually in a better position than
| the FVTC in that you can actually define the proper scheduling semantics for
| assertions in VHDL, such that any given assertion expression will get a
| consistent answer between VHDL and Verilog, for both simulation and formal
| verification.
|
| Thanks for your reply,
| -Tom
|
| > -----Original Message-----
| > From: owner-vhdl-200x@eda.org
| [mailto:owner-vhdl-200x@eda.org]On Behalf
| > Of Bailey, Stephen
| > Sent: Friday, September 12, 2003 1:45 PM
| > To: 'Tom Fitzpatrick'
| > Cc: vhdl-200x@eda.org
| > Subject: [vhdl-200x] RE: Advisory vote: simple subset of PSL
| >
| >
| > Hi Tom,
| >
| > > As a DASC member, I'd like to vote in opposition to your proposal:
| > >
| > > > > Should the assertions team continue constructing a detailed language
| > > > > change proposal based on incorporating and integrating PSL into VHDL?
| > > > >
| > >
| > > It is premature for the VHDL-200x committee to consider incorporating PSL in
| > > VHDL for two simple reasons. The first is that the Accellera Board of
| > > Directors has not donated PSL to the IEEE for consideration. Further,
| > > Accellera plans to change PSL in PSL1.1 to be compatible with
| > > SystemVerilog.
| >
| > Neither of these are a problem on the face of it given that this
| > is an advisory vote and we still have quite a bit of work to do
| > before a complete technical proposal is ready. Additional
| > responses are included below.
| >
| > First, neither the WG nor the IEEE requires that PSL be an IEEE
| > standard. The 1.01 version of PSL was approved by the Accellera
| > board as reported in the 2 June 2003 Press Release
| > http://www.accellera.org/press19.html.
| >
| > Second, we have no plan or desire to duplicate or modify the PSL
| > standard by physically incorporating it (duplicating in part or
| > whole) into the VHDL standard. It will be incorporated by
| > reference. Therefore, any Accellera (or IEEE, if PSL has been
| > donated to IEEE by then) changes to PSL up to a cut-off point
| > determined by when we (the WG) decide it is OK to ballot will be
| > automatically included. This is entirely in compliance to
| > Accellera's "Declaration of Conditions of Use Without License
| > Accellera Property Specification Language"
| > http://www.accellera.org/pslconditions.html.
| >
| > Third, the WG does not have any desire to incorporate a standard
| > that is obsolete. Therefore, I would expect the WG to make the
| > decision on when it can go to ballot to be consistent with a
| > suitably stable version of PSL. (Since the Accellera board
| > approved 1.01, it must have a reasonable level of stability.)
| >
| > > Therefore, if the VHDL-200x committee wishes to get a head-start on a simple
| > > subset of assertions, they should consider SystemVerilog assertions. The
| > > VHDL-200x committee investigation of PSL1.01, which will change, is not a
| > > prudent use of resources.
| > >
| > > If you or other committee members wish to publish articles or conference
| > > papers about ABV in VHDL, these papers should accurately reflect the
| > > situation, not promote the further perpetuation of "language wars."
| >
| > The articles do not perpetuate any language wars. The only
| > language war currently in progress is the battle between
| > SystemVerilog and 1364-2005. This WG has no opinion and takes no
| > sides in that particular war and the articles make no mention of
| > either SystemVerilog or Verilog 1364 (any version). This WG only
| > wishes to incorporate ABV capabilities into VHDL in a manner that
| > provides good value to VHDL users while being expeditious and
| > likely to be implemented by EDA vendors. Therefore, to the
| > extent that PSL and SystemVerilog Assertions evolve to be more
| > compatible with each other, that would only serve to further our
| > objectives.
| >
| > I would like to thank you for pointing out that changes to the
| > PSL LRM are planned. We will communicate with the Accellera FVTC
| > and follow their progress and plans to ensure we do not send the
| > VHDL ballot prematurely.
| >
| > BTW: You were not subscribed to vhdl-200x so your email bounced.
| > I have subscribed you to the list. For the benefit of the rest
| > of the list, I have attached Tom's original email.
| >
| > ------------
| > Stephen Bailey
| > TME, Mentor Graphic's Model Technology Group
| > sbailey@model.com
| > 303-775-1655 (mobile, preferred)
| > 720-494-1202 (office)
| > www.model.com
| >
| >
|
|
This archive was generated by hypermail 2b28 : Fri Sep 12 2003 - 15:37:26 PDT