Subject: RE: two remaining questions
From: Armoni, Roy (roy.armoni@intel.com)
Date: Tue Dec 04 2001 - 08:14:00 PST
Hi Erich,
Let me try to answer your questions, starting from the second.
The changes made to ForSpec in order to meet the Accellera requirement were
basically a few
syntax changes, plus the addition of two operators. The syntax changes are
adoption of
Verilog's Boolean expression to replace the Boolean expression layer of
ForSpec 1.0, and
some renaming of a few of the formula operators and regular expressions (for
instance, &&
instead of &) and things of that sort. The additional two operators are
"ended" and && on
regular expressions as mentioned in my presentation.
For the compilation of ForSpec, let me first say that the general approach
taken is the
automata theoretic approach for LTL model checking. You may wish to look at
the following
two excellent references:
model checking book of Clark, Grumberg and Peled for two methods of tableau
construction
and
the survey of the automata theoretic approach to LTL model checking in
Vardi's home page (if
you have problems opening it, it might be that it is because you get a .ps
file with .gzip
suffix. Try to change the suffix and open it as .ps. Moshe, you may wish
to fix that.).
At any rate, the idea is that for a formula f, we build a Buchi automaton
A(!f) that accepts the
language L(!f). If A(!f) accepts, then the trace that it accepts is a
counter example. If A(!f)
rejects, then the formula f passes.
So a step by step overview of compiling ForSpec could be:
1. Propagate clocks and resets up to the Boolean layer (annotating every
operator with the
clock and resets signals).
2. For the regular expression, build the non deterministic automaton that
accepts its language,
where !clock keeps you at the same state, and resets abort to either an
accept or reject
state.
3. For LTL operators, build the corresponding Buchi automaton, again, taking
into account
clocks and reset the same way as for regular expressions.
4. SEQ is basically concatenation of automata (the one for the regular
expressions followed
by the one for the formula). e TRIGGERS f may be compiled as either !(e
SEQ !f) if one
builds a fussy automaton, or, if a sloppy automaton is built, e should
be complemented.
Please let me know if there is anything I should elaborate on.
Regards,
Roy
-----Original Message-----
From: Erich Marschner [mailto:erichm@cadence.com]
Sent: Tuesday, December 04, 2001 12:23 AM
To: vfv@eda.org
Subject: two remaining questions
The discussion over the past two weeks has been interesting, although not
as enlightening as one might have hoped. I'm left with the impression that
the useful parts of the discussion centered on the following:
- differences between ForSpec and Sugar definitions of && on regexps
- a detailed sketch of the implementation of Sugar/Foundation Language
- a somewhat detailed sketch of the implementation of Motorola's CBV
- some level of clarification (?) about meaning/implementation of rigid
bits
- some info on support for simulation and formal verification in each
language
One concern of mine in determining which candidate languages to support
going forward has been the degree to which the donating group is willing to
discuss the implementation strategy as well as the language definition. I
think it is important for a standard language to have at least a reference
implementation sketch available as part of the standard, so that
standardization does not merely become a means of obtaining public
endorsement for proprietary software. Cindy has provided a very detailed
overview of how Sugar/Sugar Foundation Language can be implemented. John
has provided a similar level of detail about implementation of CBV. I'd
like to thank both for their openness. But I still don't have a real sense
of implementation strategy for Forspec or Temporal e. Moshe has pointed to
a few papers (which gave me postscript errors when I tried to read them),
as well as making some cryptic comments about "informative prefix" notions,
which comments are not as informative as I'd like to see. Verisity has
made no statements (that I have seen) about implementation strategy. I
would be interested to hear (more) from both Intel and Verisity about
implementation strategy.
Another concern is with the size of the language we are defining. I
believe that a standard language should be relatively small, to enable its
implementation by many vendors in a relatively short timeframe. (Or else,
if it is large, it should be layered, so that implementations of at least
some layers of it can be completed quickly.) We have agreed that the
language design teams would probably need to modify the originally donated
languages to meet the requirements we have adopted, and as a result, each
team has identified some extensions it plans to make in the next
round. But what limits will be placed on those extensions? I.e., how much
larger will each language grow, if it makes it to the next round? I'm
particularly concerned about ForSpec, which (if I understand correctly) is
being extended already to create ForSpec 2.0, which is expected to meet all
of our requirements. But how much more will it do, especially given that
the extensions are (apparently) coming from discussions with specific
partners? For that matter, what about features it already contains (e.g.,
in the clocks area) that are not required by our requirements list - will
they stay in ForSpec, or will they become optional? Similarly, I
understand that there may be capabilities of Temporal e that are outside of
omega-regular languages - i.e., that would be difficult to implement by
translating to a notation that supports exactly omega-regular
languages. What part of Temporal e, if any, would be removed, or made
optional, in the next round? I would be interested to hear from both Intel
and Verisity what restrictions they plan to make. I applaud IBM's
restriction of Sugar via defining the Sugar Foundation Language (which,
especially if you factor out the 'syntactic sugar' definitions, seems to be
quite compact indeed); I'd like to see a similar commitment to restricting,
or at least limiting the growth of, the other proposed languages.
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@home.com
This archive was generated by hypermail 2b28 : Tue Dec 04 2001 - 08:15:38 PST