Subject: RE: Similarity between ForSpec & E
From: Armoni, Roy (roy.armoni@intel.com)
Date: Wed Aug 01 2001 - 05:40:32 PDT
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 in the 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 : Wed Aug 01 2001 - 05:41:48 PDT