Checking a Liveness Property Using EBMC

What is a Liveness Property?

Liveness properties capture the intent that something useful happens eventually. A standard example of a liveness property of a circuit is that a request signal is followed eventually by an acknowledge signal. The symptom of a liveness-related bug is typically that the circuit "hangs".

Writing Liveness Properties in SVA

System Verilog Assertions offers two alternative ways to write liveness properties. The first uses the sequence syntax and the delay operator. As an example, the assertion

assert property (request |-> ##[1:10] acknowledge);

checks that the request signal is followed by an acknowledge signal within 10 transitions. The property includes a deadline (10 transitions), and is hence a bounded liveness property. When it is undesirable to fix the deadline, replace the value on the right-hand side of the colon by a $ (dollar sign):

assert property (request |-> ##[1:$] acknowledge);

As an alternative to the sequence syntax, SVA offers temporal modalities. As an example, the property above can be re-written as

assert property (request implies s_eventually[1:$] acknowledge);

Refuting Liveness Properties with Bounded Model Checking

EBMC can be used to find counterexamples to liveness properties using its BMC engine. Let us consider a simple Verilog design example5.sv together with a liveness specification.

module top(input clk);

  reg [31:0] x, y;

  initial x=0;
  initial y=0;

  always @(posedge clk) x<=x+1;
  always @(posedge clk) y<=y+2;

  p1: assert property (x==0 |-> ##[1:$] y==18);

endmodule

The following command is used to check the liveness property given in the design for traces with up to 10 transitions.

ebmc example5.sv --top top --bound 10