Formal verification is 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 serve as formal statements that describe the expected behavior or constraints of a design under verification. Formal engines classify Assertion properties into two main types: safety and liveness properties.
In this article, we will briefly describe what safety and liveness properties are and provide some practical advice on how to use them. 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:
- They describe behavior that requires a finite number of state transitions.
- They can be falsified by a finite counterexample.
- They often converge faster than liveness properties in formal verification tools.
- They are generally simpler for formal verification tools to fully prove.
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 what should happen in the future, ensuring that something good will eventually happen.
Liveness properties have distinct characteristics:
- They describe behavior that may extend infinitely into the future.
- They can only be falsified by an infinite counterexample.
- They sometimes converge faster than safety properties, but this depends on the specific property and DUV.
- They are generally harder for formal tools 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 an acknowledgment is expected 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 and 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. The choice between these two types of properties depends on the specific requirements and characteristics of the design under verification.