Safety and Liveness

Every property belongs to one of two families. A safety property says that something bad never happens: two grants at once, a lost word, a count above the limit. A liveness property says that something good eventually happens: every request is granted, every job finishes. The two need different checks and produce different counterexamples. This article explains the difference, shows why bounded model checking handles liveness through bounded deadlines, and finds a starvation bug in an arbiter.

9 min read | Intermediate

What You'll Learn

• Tell safety properties from liveness properties
• Explain why a liveness counterexample is an endless loop, not a finite trace
• Turn a liveness rule into a bounded deadline that BMC can check
• Find a starvation bug in a fixed-priority arbiter

Safety: Nothing Bad Happens

All the properties in this chapter so far are safety properties. They have one thing in common: when they fail, they fail at a specific cycle, and the trace up to that cycle proves it. A counterexample is a finite list of cycles that ends in the bad state.

a_safe: assert property (@(posedge clk) disable iff (rst) gnt != 2'b11);

Bounded model checking is built for safety. It looks for a bad state within the depth, and if it finds one, the trace is the counterexample.

Liveness: Something Good Eventually Happens

A liveness property has no deadline:

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

s_eventually means "at some point in the future, with no limit". The s_ stands for strong: the property fails if the good event never happens, even after infinitely many cycles.

Such a property can never fail at a specific cycle. After any number of cycles without a grant, the grant could still come in the next one. The only way to show that it never comes is a trace that runs forever without it. Formal tools show this as a loop: a path from reset into a cycle of states that repeats forever, and in which the grant never happens. Such a counterexample is called a lasso, after its shape.

Commercial tools can prove and refute liveness properties with special engines. Bounded model checking cannot, because it only looks at finite traces. In practice, most engineers check liveness as a bounded deadline anyway, for a good reason: a grant that comes after a million cycles satisfies the liveness property but is useless in a real system.

Bounded Liveness

A bounded version of the rule gives the good event a deadline:

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

Now the rule fails at a definite cycle: the fifth cycle after a request without a grant. It is a safety property again, and BMC can check it. It is also stronger than the liveness rule, because it demands a fast answer, not just an eventual one.

Liveness rules usually need a fairness assumption about the environment. An arbiter cannot grant a requester that gives up, so the rule only makes sense if the request stays up until it is granted:

m_hold: assume property (@(posedge clk) disable iff (rst) req[1] && !gnt[1] |=> req[1]);

The Design: a Two-Requester Arbiter

This arbiter gives a one-cycle grant to one of two requesters. Requester 0 always wins:

module arb2 (input clk, input rst, input [1:0] req, output reg [1:0] gnt);
  always @(posedge clk)
    if (rst)         gnt <= 2'b00;
    else if (req[0]) gnt <= 2'b01;      // bug: fixed priority, requester 1 can starve
    else if (req[1]) gnt <= 2'b10;
    else             gnt <= 2'b00;
endmodule

Fixed priority is not wrong in itself. But if requester 0 keeps asking, requester 1 is never served. That is called starvation. The specification here says every requester is served within 4 cycles, so this design breaks it.

Running It in ChipVerify Lab

The deadline becomes a helper counter of cycles waited, as in the sequences and implication article:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // a request is held until it is granted
  always @(posedge clk) if (!init && !$past(rst) && $past(req[0]) && !gnt[0]) assume (req[0]);
  always @(posedge clk) if (!init && !$past(rst) && $past(req[1]) && !gnt[1]) assume (req[1]);
  // bounded liveness: req[1] |-> ##[0:4] gnt[1]
  reg [2:0] wait1 = 3'd0;
  always @(posedge clk) wait1 <= (rst || gnt[1] || !req[1]) ? 3'd0 : wait1 + 3'd1;
  always @(posedge clk) if (!init) assert (wait1 <= 3'd4);
  // safety: never two grants
  always @(posedge clk) if (!init) assert (gnt != 2'b11);
`endif

The run fails at step 7:

Both requesters ask from step 1. Requester 0 wins in every cycle. In step 5 it finally drops its request, and requester 1 is granted in step 6, five cycles after it asked. A longer trace with requester 0 asking forever would be the lasso counterexample of the liveness rule. The deadline turns it into a finite trace of 8 cycles.

The safety rule passes: this arbiter never grants both. Safety and liveness are independent. A design can be perfectly safe and still starve a requester, and a design that grants everything at once never starves anybody but is unsafe.

Common Mistakes

always @(posedge clk)
  if (rst)               gnt <= 2'b00;
  else if (req == 2'b11) gnt <= (gnt == 2'b01) ? 2'b10 : 2'b01;   // round robin on a tie
  else                   gnt <= req;