Designers are typically more familiar with safety properties, whose intention is to check a “bad thing” can never happen.
For example, in the following safety property, when valid is asserted while ready is low, valid should keep asserted in the very next cycle.
assert property (@(posedge clk) vld & ~rdy |=> $stable(vld));
If valid is deasserted in the next cycle without ready being high in the current cycle, the above safety property will fail.
Liveness properties, on the contrary, are trying to prove the “good thing” will always eventually happen. The power of liveness lies in proving the infinite.
For example, in the following liveness property, when valid is high, ready should eventually be high, such that no deadlock shall happen.
assert property (@(posedge clk) vld |-> s_eventually rdy);
The table below shows a comparison between safety and liveness properties.
| Safety Properties | Liveness Properties | |
| Proof | The “bad thing” must never happen | The “good thing” will always eventually happen |
| Counterexample | The “bad thing” can happen; A finite trace shows how that happens | The “good thing” may never happen; An infinite trace shows why |
| Bounded Proof | The “bad thing” cannot happen for some number of cycles, but it might be possible in a longer trace | Currently no way to reliably infer a partial true result from an undermined liveness proof |
In the next post, we will cover how to write efficient liveness properties.
Chipress 
Leave a comment