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.