Subject: RE: Similarity between ForSpec & E & Sugar
From: Armoni, Roy (roy.armoni@intel.com)
Date: Thu Aug 02 2001 - 01:25:32 PDT
Two comments:
(1)
The linear fragment of Sugar is a proper subset of FTL.
This is in response to the misperception that ForSpec cannot express the
weak implication.
(2)
The same way Sugar can be incorporated with resets and multiple clocks,
ForSpec
can be enhanced with CTL. However, Intel does NOT WANT to mix branching
time and
linear time because of the reasons I enumerated below. We support Moshe
Vardi's
proposal to allow writing CTL properties as Motorola allow in their tools.
I say: "Branching-Linear mixture is bad. Linear time with GIGO-CTL is
better."
-----Original Message-----
From: Dana Fisman [mailto:dana@wisdom.weizmann.ac.il]
Sent: Wednesday, August 01, 2001 10:45 PM
To: Armoni, Roy
Cc: 'Bernard Deadman'; vfv@eda.org
Subject: RE: Similarity between ForSpec & E & Sugar
Roy,
you said:
>>>Finally, if what you mean by combining ForSpec and Sugar is
>>>basically taking ForSpec and augment the regular expressions
>>>with a few additional operators, then I am in favor of that.
Hold your horses... it makes more sense to go the opposite way, and
I believe that's what Bernard said a while ago. In other words, it
makes more sense, to me, to start from Sugar.
Note:
As opposed to Forspec who finds it hard to support branching constructs,
it would be quite easy for Sugar to support linear constructs. In fact,
this wouldn't be the first extension of CTL based model checker to permit
LTL specification (all based on the well known reduction of LTL model
checking to CTL model checking with firness constraints).
Also, several committee members have observed that the Sugar syntax is
more elegant and concise. Add this to the fact that branching constructs
are essential, and the conclusion is that the most reasonable unification
would be of ForSpec into the linear fragment of Sugar.
It's true, Sugar does not have the subtle support for multiple clocks
which Forspec has, nor a special treatment for reset. However, I see
many Sugar users whose designs use multiple clocks (and resets...),
and they are all content with Sugar. In IBM we decided not to support
multiple clocks, as the semantics tends to be very complicated (as can
be seen with ForSpec). Moreover, usually in multi-clocked designs, there
is no need for more than one clock per formula. In the rare cases where
there is a need to refer to two clocks in one formula, one can do it
manually. In any case, if the committee finds the clocks/reset issue
essential, there is no theoretical obstacle to include multiple clocks
and resets in Sugar. Sugar can do it.
Dana.
P.S.
I would like to comment on the similarity you suggest between
the Sugar suffix implication operators to the TRIGGERS
operator of ForSpec.
TRIGGERS resembles the STRONG suffix implication of
Sugar (r1 |-> r2!) and not the WEAK suffix implication of sugar (r1 |->
r2). The difference is crucial.
The weak suffix implication of Sugar refers to INFINITE languages, whereas
the strong suffix implication refers to FINITE languages.
My understanding is that ForSpec does not have operators similar to
Sugar's weak suffix implication.
Moreover, since the regular expressions used in ForSpec always represent
a FINITE a language, I believe it will take quite an effort from ForSpec
to incorporate such operators. These operators are very important since
they allow On-The-Fly model checking.
On Wed, 1 Aug 2001, Armoni, Roy wrote:
> Hi Bernard,
>
> The |=> operator of Sugar is similar to TRIGGERS NEXT of ForSpec.
> The |-> of Sugar is similar to TRIGGERS of ForSpec.
> However, in P45.2, the ForSpec code contain -> which is standard
> implication (f -> g is equivalent to !f | g).
> I cannot see how you compare the Sugar code with |=> to the ForSpec
> code with ->.
>
> The above of course has nothing to do with your argument that the linear
> fragment of Sugar can be combined with ForSpec. This is of course easy
> because ForSpec semantics is robust to changes in the set of regular
> operators. Actually, ForSpec does not assign semantics to regular
operators
> at all - rather, it assigns semantics to languages of finite words. Then,
> it
> combines these languages with LTL using the SEQ and TRIGGERS operators.
> Thus, any set of regular operators that create languages of FINITE words
may
> be added to ForSpec without a single change in the semantic definition.
>
> The problems arise when you look at the rest of the languages. Sugar
> involves branching time semantics and linear time semantics in the same
> formulae (look for instance at "AG {x,y*,z} (AF a)"). Intel philosophy
does
> not care much about adding CTL construct separately (as in Motorola
tools),
> but does not want to allow the mixture inthe same formula because of
> several reasons:
> (1) It affects badly the assume-guarantee paradigm.
> (2) Assigning semantics to these formulas in simulation (models of single
> finite traces) will most probably be different than in FV.
> (3) Linear time thinking is more natural.
> (4) Bounded model checking with SAT works on linear time spec.
> (5) Guiding the users to avoid using CTL operators when not needed
> because of the above reasons (for instance, with the above example of
> the Sugar formula, the user probably wanted to write
> "ALWAYS (x,y,z) TRIGGERS eventually a".
>
> Also, there are the constructs for hardware features in ForSpec (clocks &
> resets). Sugar gives a problematic definition for clocks and only for a
> single
> clock per formula. Resets are not supported at all by Sugar.
>
> Finally, if what you mean by combining ForSpec and Sugar is basically
> taking ForSpec and augment the regular expressions with a few additional
> operators, then I am in favor of that and the delta from the existing
> ForSpec is negligible. We also have no objection to Moshe Vardi's
proposal
> to have an escape route to pure CTL formulas. However, I second Moshe's
> opinion that such an end result will be more similar to E than to Sugar.
>
> Roy
>
>
> -----Original Message-----
> From: Bernard Deadman [mailto:bdeadman@sdvinc.com]
> Sent: Wednesday, August 01, 2001 3:01 AM
> To: vardi@cs.rice.edu
> Cc: owner-vfv@eda.org; vfv@eda.org
> Subject: Similarity between ForSpec & E
>
>
> Moshe,
>
> First my apologies for the delay in taking up this subject with you - it
> was only the arrival of the minutes for the Paris meeting that jogged my
> memory.
>
> I was puzzled when at least three times during the meeting in Paris you
> declared it would be far easier to combine ForSpec with E than with the
> Linear Fragment of Sugar.
>
> Thinking about this again I fear I have totally misunderstood the
semantics
> of ForSpec. I confess you claim the ForSpec semantics to be complete but
I
> would comment that as a novice in the definition of language semantics I
> find yours tough to comprehend and am concerned about their value to
users.
>
> Notwithstanding that, could you please look at the attached PDF file which
> focuses on one of the properties from the Accellera efforts and show me
> where I went wrong in my understanding of ForSpec? Can you help me
> understand why your language more closely resembles E than Sugar?
>
> Thanks
>
> Bernard
>
This archive was generated by hypermail 2b28 : Thu Aug 02 2001 - 07:58:10 PDT