Subject: [sv-ac] Accellera Property Specification Language v1.0
From: Erich Marschner (erichm@cadence.com)
Date: Tue Feb 11 2003 - 06:42:31 PST
Members of the FVTC,
We've achieved a major milestone with the completion of the PSL v1.0 LRM. This effort originally began more than four years ago (Oct 98), under the auspices of Open Verilog International (OVI). Three years ago, after OVI and VHDL International (VI) merged to form Accellera, the effort restarted in December 2000 with Harry Foster as chair. Since then we've discussed terminology, defined requirements, compiled examples, debated formalisms, considered alternatives, selected a language, and created and refined a very high-quality Language Reference Manual. The final product reflects years of hard work by all of you, but more importantly it represents collaboration, compromise, and consensus - the essential elements that make for a strong standard.
No standard is without controversy, and this one is no exception to that rule. The final FVTC vote for approval of the PSL v1.0 LRM was 10 for, 1 abstention, and 1 against. The abstention was due to one participant not having played an active role in development and review of the standard. No reason was given for the negative vote. Even so, the final FVTC ballot, following Accellera guidelines (only Accellera member companies who had attended 3 of the past 4 meetings were allowed to vote), approved the PSL v1.0 LRM with a better than 83% positive vote (or better than 90% of the non-abstaining votes). It is clear that, despite differences of opinion, we've achieved a strong consensus in support of this standard. It has been particularly gratifying to see the high degree of constructive collaboration among temporal logic experts from IBM, Motorola, ST, Sun, TransEDA, and Verisity during the creation and review of the LRM and of the PSL formal semantic definition. And it was especially good to see Moshe
Vardi's comment, "Harry, kudos on reaching this milestone!", at the completion of the ballot. We've come a long way since December 2000.
Now that we've reached this milestone, we need to plan the next steps. Normally the next steps would be to submit the PSL 1.0 LRM to the Technical Coordinating Committee (TCC) for approval, and following that to submit it to the Accellera Board for approval. Vassilios has suggested that if we want to follow the normal process, we must immediately submit the PSL v1.0 LRM to the TCC and to the Board, so they can both consider the LRM in parallel. However, Vassilios has also identified a number of actions that we must take prior to such submission. These include:
1. Removal of the reference to EDL. If EDL is part of PSL, then its features must be incorporated into the LRM, and the reference deleted. (Note that EDL has been donated to Accellera, and the March 20, 2002 definition of Sugar 2.0 included a section on EDL. However, the FVTC agreed to focus the v1.0 LRM on the Verilog flavor only, hence we did not attempt to incorporate the full details of EDL in this version of the document, and instead to just incorporate the reference, for future elaboration.)
2. Immediate review and approval of the System Verilog Assertion language proposal resulting from the DAS 2.0 Working Group (DWG) effort. This is in line with a motion passed by the Accellera Board on November 12, 2002, quoted here from the minutes of the Accellera Board of Directors:
There was an extensive discussion about PSL synchronization with the DAS 2.0
standard, and the role of the DWG task force in relation to the SystemVerilog-AC and
Formal Verification technical subcommittees.
Motion: The output of the DWG will be sent for approval by both the FV-TC and
the SVAC-TCs. Vassilios is directed to work out a timeframe for a vote. Each
group is to send feedback to the DWG.
Proposed: Stan Krolikoski
Seconded: Michael McNamara
The motion was passed unanimously.
It is becoming clear that the changes required above will take some time to accomplish. First and foremost, the FVTC has always made decisions through consensus, not by fiat, so it would be inappropriate for any of the above-mentioned actions to take place without the consent and support of the FVTC, and that will require time for discussion and voting. Second, it is important that we plan any changes carefully to make sure they are done well. For example, the potential use of EDL as a 'generic' flavor of PSL, for use in protocol modeling independent of any particular hardware description language, or for use in mixed-language designs, should be considered before we decide whether to include it or exclude it. (This capability has been specifically requested by some potential users of PSL.)
It is also the case that the DWG language proposal is not yet stable, and therefore a review of that language cannot be completed any time soon (although we can, and will, start now). In particular, Steve Meier's current draft LRM is only at version 0.8, and a number of issues have been identified in the SV-AC review of the language, notably by Adam Krolnik. Furthermore, Faisal has announced plans to form a committee to define the formal semantics of the DWG language, but no schedule for this work has been announced yet. Until a formal semantic definition for the language is available, it will be impossible for the FVTC to understand in detail what the DWG is proposing.
The goal of the DWG effort has been to develop a System Verilog assertion language that would be 'compatible' with both PSL and OVA, to minimize confusion among users who must deal with two or more of these languages. In fact, the DWG intially focused on identifying a common subset of features that are shared by both languages. Additional features that are not part of the common subset have been added more recently, such as the ability to define assertions in separate files, in a manner that overlaps functionally with PSL but involves a very different approach. Additions of this sort have complicated the question of what exactly the "unified kernel" is considered to be, and they may make it more challenging to achieve alignment between PSL and SVA. At the same time, some new ideas in the DWG proposal (e.g., delays in addition to repeats) will fit well into the PSL framework, and some FVTC members are already looking into how such new ideas can be added to PSL.
In summary, it appears that at this point we must turn our attention to developing PSL v1.1, which will be focused on alignment with System Verilog Assertions to minimize syntactic and semantic conflict between the two. To that end, the FVTC as a whole, and FVTC members as individuals, need to do the following:
1. Work with the SV-AC to help identify and bring to closure all of the issues with the SVA LRM. (This is already under way.)
2. Participate in the SVA formal semantics committee to ensure that SVA is well-defined.
3. Work with the SV-AC to define the extent of the "unified kernel" - e.g., whether procedural assertions should be part of PSL.
4. Develop proposed PSL changes to incorporate SVA features into PSL
5. Plan to release a PSL v1.1 LRM within 1-2 months after the SVA LRM stabilizes - hopefully by DAC 2003
At the same time, three years (or more) is a long time to be working on this standard without confirmation that it is moving in the right direction. Just as System Verilog 3.0 was approved by the Board as a baseline for the development of System Verilog 3.1, it would be appropriate for the Board to consider approving PSL v1.0 now, both as a baseline for development of PSL v1.1, and to recognize and acknowledge the significant effort that has gone into completion of this major milestone, as well as the high quality of the standard that has resulted from those efforts.
To that end, we plan to submit the Accellera PSL v1.0 LRM to the TCC and request that the TCC approve the document as it stands, to lay the groundwork for the next phase of development of this standard. At the same time we plan to submit the PSL v1.0 LRM to the Accellera Board and request that the Board approve both the LRM and the above-mentioned roadmap for development of PSL 1.1.
Regards,
Harry Foster, FVTC Chair
Erich Marschner, FVTC Co-Chair
-------------------------------------------
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
This archive was generated by hypermail 2b28 : Tue Feb 11 2003 - 06:43:39 PST