Subject: final version of safety and liveness definitions
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Tue Oct 15 2002 - 08:43:12 PDT
Following up my action on acceptable versions of the
definitions of safety and liveness in the LRM, I have
been in touch with all those who commented on the original
proposals. We have agreed on the definitions below. These
will go in the LRM, in section 3.1 and section 4.4.2,
unless there are extremely strong objections at this stage.
It is recognized that these are not key issues for the LRM,
and while the definitions must not be erroneous, they
should be concise rather than comprehensive.
3.1.39 safety property: A property that specifies an invariant over the states in a design.
The invariant is not necessarily limited to a single cycle, but it is bounded in time.
Loosely speaking, a safety property claims that "something bad" does not happen.
More formally, a safety property is a property for which any path violating the
property has a finite prefix such that every extension of the prefix violates the property.
For example, the property, "whenever signal req is asserted, signal ack is asserted within
3 cycles" is a safety property.
This definition mentions "prefix", and a definition of prefix is therefore
also required. this is given in terms of "extension", which has to be used
elsewhere in the manual for other purposes. The following definitions
of extension and prefix have been agreed:
extension: an extension of a path is a path that starts with precisely the succession
of states in the given path.
prefix: a prefix of a given path is a path of which the given path is an extension.
The final proposed definition of liveness is:
3.1.23 liveness property: claims that "something good" eventually happens. More formally,
a liveness property is a property for which any finite path can be extended to a path
satisfying the property. For example, the property "whenever signal req is asserted,
signal ack is asserted some time in the future" is a liveness property.
Some reservations have been expressed about the sentence beginning "more formally":
- it isn't very clear what it means;
- liveness for branching time logic isn't just a matter of liveness on paths;
- the definition includes questionable "liveness" properties such as "there are
more occurrences of a than b".
In general, the feeling is that this definition captures well enough the main
point about liveness, and should be left as it is. We will not accept any
modifications to the "More formally ... " sentence. If there are still strong
objections to this sentence, we may consider omitting it completely, leaving just
the general description of the notion of liveness and the example. A decision
will be made at next Monday's meeting of the review group.
Anthony
-- Anthony McIsaacSTMicroelectronics Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ
Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910
Email: Anthony.McIsaac@st.com
This archive was generated by hypermail 2b28 : Tue Oct 15 2002 - 08:47:57 PDT