Subject: LRM Review - Status Report - 12 Dec 2002 - third try
From: Erich Marschner (erichm@cadence.com)
Date: Fri Dec 13 2002 - 13:44:25 PST
Members of the FVTC,
As you are aware, the LRM Review subcommittee has been meeting weekly since September 2002 to review and refine the Sugar Formal Property Language Reference Manual, v0.8, which was developed over the summer to capture the Sugar 2.0 language definition (March 20, 2002) in IEEE LRM form.
The LRM review has now completed. What remains is updating the draft LRM with a moderately large number of relatively small changes that were identified as necessary during the review period. These changes include correction of typos, rewording for clarity, addition of illustrative examples, correct definition and consistent use of terminology, and consistent use of fonts and stylistic conventions.
As part of the review, the LRM Review subcommittee also did a very careful and thorough review of the formal definition of the language semantics. Some problems with the semantic definition were identified in that review, and the subcommittee discussed various solutions in great detail. The subcommittee has proposed a few changes to the formal semantic definition to address these issues. A summary of the issues and the proposed solution appear below. The proposed solution will be incorporated into Appendix B of the v1.0 LRM.
Application of the abovementioned changes to the v0.8 LRM will be going on through the rest of this month. The v1.0 version of the Accellera Property Specification Language (i.e., Sugar) LRM will be distributed to the FVTC in early January. The FVTC will meet in the third week of January to discuss the final LRM. The exact time and date of the meeting will be announced in early January.
I would like to take this opportunity to thank the members of the LRM Review subcommittee for the significant amount of time and effort they have invested in perfecting the Language Reference Manual. Their extensive expertise, diligent analysis, commitment to cooperation, patience, and professionalism have all contributed to making a difficult and tedious job not only tolerable, but enjoyable.
Regards,
Erich Marschner
LRM Review Subcommittee Chair
------------------------------------------------------------------------
LRM formal semantics:
status and recommendations of the review subcommittee
Summary:
A subcommittee was chartered to review the LRM of PSL Revision
1.0. During its review of the formal semantics [1], a small number
of problems were uncovered. After thoroughly investigating these
issues, the subcommittee unanimously recommends that a semantics be
adopted for Revision 1.0 of PSL that differs from the Sept 12
version in the following:
(1) the recommended semantics provides a simpler clocking scheme
than that of the Sept 12 semantics, and
(2) the recommended semantics corrects minor errors in the
Sept 12 version.
The recommended change has minimal impact on the PSL user while it
corrects errors and lays a sound basis for future enhancements.
The subcommittee has a proposal for one enhancement, in which the
complexity issue of the abort operator is addressed, and it
unanimously recommends deferring the addressing of this issue to
future revisions.
Regards,
The LRM review subcommittee, whose members are:
Cindy Eisner,
Dana Fisman,
John Havlicek,
Adriana Maggiore,
Erich Marschner,
Anthony McIsaac, and
David Van Campenhout.
------------------------------------------------------------------------
LRM formal semantics:
status and recommendations of the review subcommittee
In the review of the formal semantics in the Sept 12 LRM [1] a small
number of errors and anomalies have been identified; they can be
classified as follows:
I1. errors, e.g., the lack of duality of untils [2], and the flaw in
the definition of the 'and' operator [3].
I2. intuitive and consistent way to relate formal verification and
simulation. For a finite path, there are two, both useful, views
on the interpretation of a formula: one is to evaluate the formula
based on what is actually seen in the path, the other is to interpret
it based on what may happen on an extension of that path.
I3. computational complexity of abort and a related problem with
weak suffix implication. The simple definition of the abort operator
given in the Sept 12 semantics makes it prohibitively expensive to
evaluate certain exotic formulae [4,5] involving nested aborts.
Issues I1 and I2 have their roots in the clocking mechanism. The
subcommittee considered at great length two candidate solutions to
address these issues.
SEM_SW: this is basically the original Sept 12 semantics, modulo
a small number of corrections to address I1 and I2. The fixes
turned out to be straight-forward and very minor. In this semantics
the strength of a clock applies throughout a formula, and not just to
finding a first clock tick.
SEM_1 [6]: this semantics is obtained from the Sept 12 semantics by
simplifying the semantics of the temporal layer so that the strength
of the clock applies only to finding the first tick. This can be
achieved by making this simplification in all the definitions, and no
other changes, apart from the correction of small errors. The
clocking semantics for singly-clocked standard LTL formulas in SEM_1
is identical to those of ForSpec, and very similar to that of CBV.
Both approaches fully address I1. Both partially address I2, but in
different ways. Neither addresses I3, which we propose to address in
a future revision of the LRM.
Issue I2 is addressed only partially by SEM_SW and SEM_1, and they do
so in a different way:
- SEM_SW allows to make the useful distinction between failures due
to the design and failures due to the clock. Further, satisfaction of
a formula on a finite path, or a path with only finitely many clock
ticks, can be viewed in terms of evidence about whether the formula
can be violated if the path is extended. In this way SEM_SW supports
a consistent interpretation of formulae between formal verification
and simulation (I2) . In particular, a formula that passes in formal
verification will not fail in simulation, as either an assertion or
an assumption, if it is under a weak clock.
SEM_SW lacks a sufficiently intuitive interpretation of formulae over
finite paths in terms of what is actually seen (first view in I2).
In particular, a formula (eventually! b) holds on every finite path
under a weak clock; and (always b) does not hold on any finite path
under a strong clock.
- SEM_1 offers a sufficiently intuitive interpretation of formulae
over finite paths in terms of what is actually seen, and supports
the interpretation of a formula on a finite path in terms of what
may happen on an extension of that path (the second view in I2) via
the abort operator. So, SEM_1 does not fully address I2 because it
does not address I3.
For Revision 1.0 of the LRM, the subcommittee recommends that SEM_1 be
adopted. That SEM_1 has a more intuitive interpretation on finite
paths, is simpler, and forms the foundation for the
Neutral/Truncated/Untruncated Semantics (see below), was deemed more
important than the closer affinity to the Sept 12 semantics of SEM_SW.
For Revision 1.1 of the LRM, the subcommittee recommends that an
augmentation of SEM_1 is considered. This augmented semantics, which
has been designated Neutral/Truncated/Untruncated Semantics [7], fully
addresses both views of I2, and furthermore provides a natural and
elegant definition of the abort operator that fully addresses I3.
Basically, SEM_1 provides the neutral interpretation, in which a
formula is interpreted on a finite path based on what is actually
seen. In addition, the Neutral/Truncated/Untruncated Semantics, also
provides two dual interpretations of a formula on a finite path in
terms of evidence for what may happen on an extension of that path.
The Truncated/Untruncated/Neutral semantics addresses I2 in a much
more elegant and direct way than known semantics, in which I2 is
addressed indirectly through clock strength.
Regarding I3, it was noted that the non-elementary blowup due to
aborts will only show up in exotic formula with nested aborts, which
is certainly beyond the scope of average users. One way to address I3
is to define abort syntactically as in ForSpec. This involves defining
each operator with respect to a context that includes two reset
signals. As the much increased complexity of such semantics
definitions is undesirable, the subcommittee has sought after
alternative solutions [7]. However, it was deemed that recommending
this solution [7] for PSL Rev 1.0 would compromise the schedule for
delivering Revision 1.0 of PSL LRM as that solution is not yet
complete.
Therefore, the subcommittee recommends that (1) the definition of the
semantics of abort is left unchanged for now, and (2) issue I2 is
acknowledged in the LRM, and (3) a note is added to the LRM stating
that future revisions will fully address I2 and I3.
In summary, the subcommittee is unanimously recommending that
(1) SEM_1, which simplifies the clocking semantics of the Sept 12
version, and makes some minor corrections to it, be adopted as formal
semantics for PSL Revision 1.0, and
(2) a note is added to the LRM that acknowledges the computational
complexity due to the current (unchanged) definition of the abort
operator and that future revisions of the LRM will properly address
this issue.
The recommended change to the formal semantics mainly impacts those
who build tools based on PSL, but that impact is very small if the
clock operators are implemented via re-write rules. For writers of PSL
specifications the change will be hardly noticable because it is
manifested primarily in corner cases. This point is further supported
by the finding of the subcommittee that the change does not require
any significant modifications to the informal semantics.
References:
[1] Sugar formal property language reference manual. Version 0.8
Sept 12, 2002, Appendix B.
[2] J. Havlicek, "flaw in Sugar clocked until semantics," Oct 22
2002, http://www.eda.org/vfv/hm/
[3] D. Van Campenhout, "Sugar LRM -- more flaws in clocked
semantics," Oct 24 2002, http://www.eda.org/vfv/hm/
[4] M. Vardi, "RE: Sugar LRM -- more flaws in clocked semantics,"
Nov 01 2002, http://www.eda.org/vfv/hm/
[5] R. Armoni, D. Bustan, O. Kupferman, M. Y. Vardi, "Aborts
vs. Resets in linear temporal logic,"
http://www.cs.rice.edu/~vardi/misc/abortreset.pdf.
[6] C. Eisner, D. Fisman, M.J.C. Gordon, J. Havlicek,
A. McIsaac, and D. Van Campenhout, "Proposal for Sugar 2.0
temporal layer formal syntax and semantics SEM_1," Dec 10 2002,
http://www.eda.org/vfv/docs/formal_semantics_standalone.pdf.
[7] C. Eisner, D. Fisman, J. Havlicek, Y. Lustig, A. McIsaac, and
D. Van Campenhout, "Truncated/Untruncated semantics," Dec 10 2002,
http://www.eda.org/vfv/docs/truncated_semantics.pdf.
-------------------------------------------
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 : Fri Dec 13 2002 - 13:45:41 PST