Chipress

Liveness property debug may often be tricky. If we ever find a liveness property failure, it does not necessarily mean a deadlock exists in the design. Instead, it could be due to lack of proper assumptions.

Assuming we have a data processing block, in which both input and output data interfaces follow Valid-Ready protocols. We want to prove that, there is no deadlock in the input data interface:

assert property (@(posedge clk) vld_in |-> s_eventually rdy_in);

We could get a counterexample for the liveness property above. The problem is that the output data interface may never be alive, i.e., the tool may assume “rdy_out” is always low.

In this case, by adding a liveness assumption at the output data interface, the counterexample will be gone:

assume property (@(posedge clk) vld_out |-> s_eventually rdy_out);