Subject: RE: [sv-ac] Mathematical semantics for the upcoming sv-ac LRM
From: Erich Marschner (erichm@cadence.com)
Date: Mon Nov 04 2002 - 08:57:43 PST
Faisal,
As you know, the DWG has been trying to identify the common semantics between Sugar and OVA. It has become fairly clear that there are semantic issues that cannot be resolved easily this way. In fact, there are two, related but somewhat independent, semantic issues to be considered. First, exactly what are the semantics of declarative assertions? This includes dealing with the multiple-clock issues that we've discussed in the DWG, i.e., to what extent does the language support specification of behavior in multi-clock environments, and what "synchronization" of clocks, if any, is required by the language to handle multi-clock behavior? Second, how do procedural semantics and declarative semantics relate? I.e., if the user writes the same expression in a procedural context or in a declarative context, do they mean the same thing, or do they mean different things - and if different, how so, and why?
Accellera already has one group that is actively looking at the formal semantics of declarative assertions. In the FVTC, the LRM Review subcommittee has been examining quite closely the formal semantics of Sugar declarative assertions. There are at least five formal semantics experts participating in that review, the primary contributors being John Havlicek, David Van Campenhout, Anthony McIsaac, Dana Fisman, and Cindy Eisner. This group of semantics experts has already established a very productive working relationship and a terminology framework within which they have been able to communicate clearly about the semantics of declarative assertions. It makes little sense to try to duplicate this effort again elsewhere, so I would suggest that you leverage this group to address the multi-clock declarative semantics issues mentioned above. The same group could then address the relationship between declarative and procedural assertions semantics, once the declarative semantic basis is stable.
After all, for a long time the FVTC has been identified as being more focused on formal semantics than the SV-AC. Perhaps now that the SV-AC has finally realized the need to seriously consider formal semantics, we can find an appropriate role for the FVTC in the development of System Verilog assertions.
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: Faisal Haque [mailto:fhaque@cisco.com]
Sent: Monday, November 04, 2002 10:32 AM
To: sv-ac@eda.org
Subject: [sv-ac] Mathematical semantics for the upcoming sv-ac LRM
As part of the process to drive towards a complete LRM. We have a need for a technical subgroup to
author the mathematic semantic support for the LRM. Qualified volunteers with experience writing formal
semantics are solicited to create semantic support for the LRM. Charter is to write the semantics support but not change the language. Any language issues should be brought to DWG for resolution.
I would prefer the members of this subgroup to be other than those folks participating in DWG. If you are interested please send me an email.
Thanks,
-Faisal
This archive was generated by hypermail 2b28 : Mon Nov 04 2002 - 09:02:17 PST