Checking a Bounded Liveness Property Using EBMC

EBMC can be used to check liveness properties with a bounded semantics. 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 verify the liveness property of the design.

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

Note that the design contains a SystemVerilog assertion with an eventual operator ##[1:$]. We use the command-line option --bound to specify a bound of ten. Any bound less than ten leads to a counterexample for the property, as the variable y is incremented by two and thus, the unwinding bound must be greater than or equal to ten (nine for transitions and one additional time frame for the initialisation) for the variable y to reach 18.