Safety vs Liveness properties in formal verification
Safety vs Liveness properties in formal verification are a crucial aspect of ensuring that digital systems behave as expected under all possible conditions.. It relies on specifying and verifying properties to ensure the correctness of a design. These properties act as formal statements that describe the expected behavior or constraints of a design under verification. Formal engines divide assertion properties into two main types: safety and liveness properties.
In this article, we will briefly describe what Safety vs Liveness properties are and provide some practical advice on how to use them in formal verification. However, the theory behind these two properties is extensive and beyond the scope of this article.
Safety Properties
Safety properties ensure that the system never reaches an undesirable state, meaning that something bad will never happen.
Safety properties have several key characteristics:
- Safety properties describe behavior that requires a finite number of state transitions.
- A finite counterexample can falsify them.
- In many cases, they converge faster than liveness properties in formal verification tools.
- Formal verification tools can generally prove them more easily.
An example of a safety property is:
property property_safety;
request |-> ##[0:5] ack;
endproperty
Liveness Properties
Liveness properties guarantee that a desired outcome will eventually occur in the system. These properties focus on future behavior and ensure that something good eventually happens.
Liveness properties have distinct characteristics:
- Liveness properties describe behavior that may extend infinitely into the future.
- An infinite counterexample is required to falsify them.
- In some cases, these properties converge faster than safety properties, depending on the design under verification (DUV).
- Formal verification tools generally find them harder to fully prove.
An example of a liveness property is:
property property_liveness;
request |-> s_eventually(ack);
endproperty
Consider a scenario where a request signal is issued, and the system expects an acknowledgment in response. A liveness property would assert that eventually the acknowledgment signal will be asserted following a request. If the acknowledgment never shows up, this shows a deadlock scenario in the design.
Safety vs Liveness Properties
Now it’s time to answer the question in every formal verification engineer’s mind is which type of property should I use for my DUV. Both property types have their pros and cons:
- Using safety properties would require a lot more in-depth knowledge of the design, compared to liveness. Since you are not defining the eventual expected behavior, you need to define the situations where the expected behavior may happen along with adding accompanying assumptions to keep the expected behavior finite.
- The Cone of Influence of a liveness property is much wider than safety property, which means fewer liveness properties needed compared to safety properties for the same check. However, this can come with a downside of difficulty to get convergence in liveness properties vs safety.
- In some cases, getting convergence on a liveness property requires heavy abstraction and black boxing compared to safety properties
In conclusion, understanding the differences between Safety vs Liveness properties is essential for effective formal verification.. Safety properties ensure that a system avoids undesirable states, making them easier to verify but often requiring a deeper understanding of the design. Liveness properties, on the other hand, ensure that desired outcomes eventually occur, typically involving broader checks but often posing greater challenges in achieving convergence. Engineers choose between these two property types based on the specific requirements and characteristics of the design under verification.