Safety Properties#

Safety: Ensures that bad things never happen. Examples include:

• FIFO does not overflow.
• The system does not allow multiple processes to modify shared memory simultaneously.
• A request receives a response within 5 clock cycles.

Formally, a safety property ensures that any violation has a finite prefix such that every extension of this prefix also violates the property. Safety properties can be falsified using finite simulation runs.

Liveness Properties#

Liveness: Guarantees that good things eventually happen. Examples include:

• A decoding algorithm eventually terminates.
• Every request eventually receives an acknowledgment.

Formally, a liveness property ensures that any finite path can be extended to satisfy the property.

Assertion: Property P must eventually hold true after a triggering event occurs.

Theoretically, liveness properties can only be falsified using infinite simulation runs. In practice, we often assume “graceful test termination” to represent infinite time.

• If the good event does not occur within the test duration, we assume it will never occur, and the property is considered falsified.

Bounded Liveness#

Assertion: Property P must hold true after the start trigger event and before the end trigger event.

Invariants#

Invariant Assertion Window: Property P is checked and expected to hold after the start event occurs, and continues to be checked until the end event occurs.