Should You Use Liveness Properties in the First Place?
Liveness properties are often more complex to prove, and challenging to debug. Plus, they may not be useful in simulations (covered in the next post). Before writing liveness properties, designers should ask themselves, is it really necessary to use liveness properties in the first place?
In fact, many times, safety properties should be your first choice. For example, to verify a round-robin arbiter should never starve one request, instead of using liveness properties for each request, one can rewrite the SVA like this: “If a request is asserted, it must be granted within N cycles, where N is the total number of requests to this arbiter”.
Designers should only consider using liveness properties, only if:
- There exists a complicated set of interacting FSMs
- Rare failures happening after long period in simulation or post-silicon validation
- Deadlocks observed but not yet explained, etc.
Write Liveness Properties Properly
Most liveness properties take one of the following forms:
x |-> s_eventually y
x |-> y[->1] // non-consecutive exact repetition
x |-> y s_until z
You may see the following coding style in old RTL:
# Avoid this coding style
assert property (x |-> ##[0:$] y)
Such coding style should be avoided, since it is “weak” by default, and it is not required to be true on infinite traces.
In SVA 2005, this was the only way to express liveness. But in SVA 2009+, this was no longer accepted.
In legacy RTL, if changing the coding style is not possible, one can make it “strong” to enforce proof to infinity by:
elaborate … -sv09_strong_embedding
Avoid Mixing Safety and Liveness Together
Liveness property is by itself already complicated enough. Designers should avoid mixing safety and liveness in a single property. For example, instead of writing something like this:
x |-> y ##[0:$] z
Split the property into two: one for safety, and the other for liveness.
Chipress 
Leave a comment