Subject: pending sugar issues
From: eisner@il.ibm.com
Date: Wed May 09 2001 - 05:32:44 PDT
all,
following are responses to some of the issues that were raised during the
sugar presentation on may 3. if i missed anything, or if you have other
questions, please don't hesitate to ask.
1. ed clarke asked if the sere operators ~ and && can be viewed as
syntactic sugar. the answer is yes. for instance, see [1] for a
definition of ~ in this manner. we find the direct definition of the
semantics to be more intuitive than a definition as syntactic sugar, thus
we chose to define them this way in the document "the syntax and semantics
of sugar" previously distributed to the committee. note also that a direct
implementation will be much more efficient than an implementation as
syntactic sugar.
2. limor fix pointed out that the use of the weak until operator in the
definition of "EX q::clk=clka" given on page 24 is problematical, because
for "AX q::clk=clka" we get that the clock is required to tick on every
path. the answer is that a clocked EX formula should use the strong until
operator instead of weak until. thus, "EX q::clk=clka" requires that there
be a path such that there is a next tick, just as "EX q" requires that
there be a path with a next state. then for "AX q::clk=clka" we get that q
is required to hold on all next ticks, without the requirement that there
be such a tick on every path. the complete formal definition of clocked
sugar formulas is attached.
3. bernard deadman pointed out that in the pci examples, i used signals
such as "frame_fall", while in actuality there is probably no such signal
in the design. in fact, rulebase allows reference to such edges through
the built-in functions prev, rose, and fell. prev(sig) is valid if and
only if signal "sig" was valid in the previous state, rose(sig) is valid
if and only if signal "sig" was invalid in the previous state and is valid
in the current state, and fell(sig) is valid if and only if signal "sig"
was valid in the previous state and invalid in the current state. since
these built-in functions may be called from sugar formulas, they can be
considered part of the syntactic sugar. so the pci examples could have
been coded used "fell(frame)" instead of referring to the non-existent
signal "frame_fall".
4. in a follow-up email, bernard deadman asked, "Can you save and
subsequently access the previous address value from within the temporal
expression? Does Sugar support the ability to allocate and reference
variables?" again, the answer is that rulebase allows something like this,
and in fact this feature, like the built-in functions, can be viewed as
part of the syntactic sugar. so, we can say
forall dbit: boolean: formula { AG ((write & (data_bus(0)=dbit) ->
next_event(read)(data_bus(0)=dbit)) }
or,
forall dbits(0..31): boolean: formula { AG ((write &
(data_bus(0..31)=dbits(0..31)) ->
next_event(read)(data_bus(0..31)=dbits(0..31))) }
in these examples, dbit and dbits(0..31) can be viewed as auxiliary state
variables which "awake" non-deterministically and thereafter hold their
value steady.
5. in the same email, bernard asks to see the sugar encoding of some of
the properties from the list i sent. i promise to get to this very soon,
and will send sugar for all properties on the list to the entire group.
as i said before, if i forgot something, or if you have additional
questions, please let me know.
regards,
cindy.
[1] I. Beer, S. Ben-David, and A. Landver. On-the-fly model checking of
RCTL formulas. In Proc. 10th International Conference on Computer Aided
Verification (CAV), LNCS 1427, pages 184-194. Springer-Verlag, 1998.
(See attached file: sugar_clocks.ps)
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-855-0070
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
This archive was generated by hypermail 2b28 : Wed May 09 2001 - 05:35:07 PDT