Definition

Liveness verification is the verification of whether a system can avoid getting into a state where it never makes forward progress. In the cited microprocessor-verification context, liveness is needed to show that a pipelined processor does not stall indefinitely. [1]

Role in formal verification

Liveness verification complements safety-oriented checks. The evidence describes a case where a pipelined microprocessor may pass a verification condition even when it deadlocks, because the verification can tolerate pipeline stalls caused by hazards or instruction cancellations caused by mispredicted branches. In the extreme, a device that does absolutely nothing could pass such a verification. Therefore, completing the verification requires a liveness proof that rules out non-progressing states. [1]

Example: pipelined microprocessors

In the UCLID5-based verification of pipelined Y86-64 microprocessors, the modeled system combines a pipelined microprocessor with a sequential reference implementation, and the verification script describes how to initialize and operate the system and which verification conditions to check. Within that setting, liveness is used to prove that the pipeline cannot stall forever. [1]

Relationship to safety properties

The cited report describes an approach for proving liveness that builds on a safety property. The goal is not merely to show that each observable behavior is safe, but also to show that the processor continues making progress rather than remaining indefinitely stalled. [1]