TABLE OF CONTENTS The abort operator is used to describe reset functionality. For example, consider the case that we want to state that every request is followed by an acknowledge, except that if a reset occurs, we are not required to see the acknowledge. Assuming that a request is indicated by an assertion of signal req, an acknowledge by an assertion of ack, and a reset by an assertion of rst, we could use Property 7.1a to express our specification. Property 7.1a holds on Trace 7.1(i) because every request is eventually followed by an acknowledge, except for those requests that are aborted by a reset.
NOTE: The right-hand operand of an abort operator (the abort condition) must be a Boolean expression.
In our simple example, the utility of the abort operator is not immediately apparent because we could have written the same property without it, as shown in Property 7.1b. However, it is not always easy to do the same for other properties. For example, consider Property 7.2a. If we want to indicate that an assertion of rst cancels the right-hand side, we would have to break the righthand side into pieces, as shown in Property 7.2b. The abort operator allows us to express Property 7.2b in a much simpler manner, as shown in Property 7.2c. The idea behind the abort operator is that up until the assertion of the abort condition, everything must "go...
