Liveness, Fairness, Deadlock

Fairness: The Stall Always Ends

A liveness property (F1.5) fails on a loop, not at a step. Most such failures on a correct design are the environment's: the solver holds ready low forever, and no design can grant. A fairness constraint is a liveness assumption on the environment: assume property (@(posedge clk) s_eventually ready); says the stall always ends, without saying when.

Liveness without fairness fails on almost everything. Fairness that is never checked hides almost everything, which is why a live job needs a sanity run (below). The editor here runs the bounded forms; liveness itself is drawn, not run.

The $fell form fails because ready can be low from reset: it never falls, so the assumption never starts. The two-cycle bug fails under fair stalls too, because ready may rise for one cycle at a time. Bounded response is weaker than liveness, since it invents a deadline the spec may not state, and far cheaper.

Three Ways to Make No Progress

A deadlock is a safety property in disguise: one stuck state, reached at a finite step, so bmc finds it. Livelock and starvation have no bad state; every state on the loop is legal and only the loop is wrong (A3.1 Weak and strong).

Three Rules for a Live Job

Written out, the live job is assert property (@(posedge clk) req |-> s_eventually gnt); with assume property (@(posedge clk) s_eventually ready);, alone, plus the sanity job. When a liveness proof will not converge, the bounded form above is the common substitute; record the deadline you chose as a reviewed assumption.

Asked in Interviews

Try It

assert property (@(posedge clk) req |-> s_eventually gnt);
assume property (@(posedge clk) s_eventually ready);
// sanity job, must FAIL:
assert property (@(posedge clk) s_eventually 1'b0);

assume property (@(posedge clk) disable iff (rst) !ready |-> ##[1:4] ready);
assert property (@(posedge clk) disable iff (rst) req |-> ##[1:8] gnt);

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv props.sv
prep -top hs_live
[files]
design.sv
props.sv

1. Run without fairness

   Run as it is: FAIL at reported step 10. Count the window steps with ready low.

2. Add bounded fairness

   Add the !ready |-> ##[1:4] ready assumption as the first line of props.sv: BMC PASS to depth 20.

3. Try the $fell form

   Write it as assume property (@(posedge clk) disable iff (rst) $fell(ready) |-> ##[1:4] ready); with the registered ready_q. Why does it not help?

4. Ask the spec

   What deadline does the spec actually state for the grant? What did the bounded form add?

5. Find the deadlock

   Run two_fsm as safety: FAIL at reported step 3. Then make both machines take lock 1 first.

Check Yourself

module hs_live(input clk, rst, req, ready, output reg gnt=0);
  reg pending=0;
  reg ready_q=0;   // last cycle's ready
  wire go = (pending || req) && ready;
  always @(posedge clk) begin
    ready_q <= ready;
    if (rst) begin pending <= 0; gnt <= 0; end
    else begin
      gnt <= go;
      if (go) pending <= 0;
      else if (req) pending <= 1;
    end
  end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
`endif
endmodule

assert property (@(posedge clk) disable iff (rst) req |-> ##[1:8] gnt);