Subject: Re: Branching Time
From: eisner@il.ibm.com
Date: Sun Jul 08 2001 - 07:20:43 PDT
moshe,
>I do not see, however, how Sugar captures the
>English.
the decision taken in the sub-committee was that, since english is
ambiguous, the temporal logic formulation (of the language used by the
submitter of the property) will be the specification. the only exceptions
were properties 45.x, because they relate to the well-known pci
specification.
>Take, for example, Property 63: "Lack of dealock". Sugar says
>
>AGEF (state=idle)
>
>This says that at any given state there is a sequence of inputs that
>lead to idle. It is definitely possible, however, that a certain input
>value is not acceptable by the system, leading to deadlock.
>
>A much simpler property expressing lack of deadlock is
>
>AG !deadlock.
one is a liveness property, the other is a safety property. surely you are
not suggesting that the two are equivalent?
>I suspect that Property 64 suffers from he same problem, but I don't
>quite understand the English there.
again, the sugar is the specification, not the english. to help your
intuition as to what this spec is trying to check, perhaps the following
will help:
In PCI read transactions, the target should not depend on the master to
assert its TRDY_ signal. That is, the target should not wait for the
assertion of IRDY_ before it asserts TRDY_. The Sugar specification simply
states that there exists a path where the TRDY_ is asserted before IRDY_.
regards,
cindy.
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 : Sun Jul 08 2001 - 07:14:55 PDT