EBMC – A Short Tutorial

Introduction

We assume that you have already downloaded the EBMC binary on your system. If not, please download the EBMC binary from here. Or consider the web version.

Given a synthesizable hardware design in Verilog at register transfer level (RTL) and safety or liveness properties given in the property specification language SVA (SystemVerilog Assertions), EBMC verifies the correctness of the design with respect to the property. EBMC can perform both bounded and unbounded verification. In this brief tutorial, we demonstrate how to apply EBMC to Verilog designs for bounded verification. Methods for unbounded proof are described here.

Checking a Combinational Circuit Using EBMC

Let us consider a simple combinational circuit example1.sv. It implements a two-bit adder. The design comes with a test harness, which includes a SystemVerilog assertion. The assertion checks the result computed by the adder.

module my_add(input a, b, output [1:0] y);

  assign y[0]=a^b;
  assign y[1]=a&b;

endmodule

module main(input a, b);

  wire [1:0] result;

  my_add adder(a, b, result);

  assert final (2'(a)+b==result);

endmodule

The following command is used to run EBMC to verify the correctness of the combinational circuit.

ebmc example1.sv --top main

Observe that we have specified the name of the top-level module using the --top option. In response, EBMC reports "PROVED up to bound 1" for the property, which means that it holds for any inputs a and b.

Property Specification on the Command Line

EBMC also allows to specify a property on the command line. For example1.sv, we can specify our property on the command line as given below.

ebmc example1.sv --top main -p "a+b==result"

Bounded Verification of a Sequential Circuit Using EBMC

The behavior of a sequential circuit not only depends on the inputs but also on the state of any registers or flip-flops. We can instruct EBMC to perform bounded verification of a sequential circuit up to a desired depth by giving the --bound command-line option. EBMC then proves or refutes the assertions by considering all executions that are no longer than that bound.

To illustrate bounded verification, let us consider a simple Verilog circuit for counter design named example3.sv. The design contains two SystemVerilog assertions. The first assertion checks that the least-significant bit of the counter flips when the input named enable is high. The second assertion checks whether the counter can reach the value three.

module counter(
  output [7:0] out,
  input enable, input clk);

  reg [7:0] state;
  assign out = state;

  initial state = 0;

  always @(posedge clk)
    if(enable)
      state = state + 1;

  assert property (enable && state[0] |-> ##1 !state[0]);
  assert property (state!=3);

endmodule

Now, run EBMC command to verify the counter circuit for ten transitions as follows:

ebmc example3.sv --top counter --bound 10  

EBMC reports that the first assertion holds, and that the second assertion has failed, as follows:

** Results:
[counter.property.1] always counter.enable && counter.state[0]
                     |-> ##1 !counter.state[0]: PROVED up to bound 10
[counter.property.2] always counter.state != 3: REFUTED

We can obtain a counterexample trace that demonstrates how the second assertion is violated by adding the option --trace to the command line.

Specifying the Reset Logic

Let us consider a variant of the Verilog model, given as example4.sv. In this variant, the initialization of the registers is performed using an active-high, synchronous reset signal.

module counter(
  output [7:0] out,
  input reset, input clk);

  reg [7:0] state;
  assign out = state;

  always @(posedge clk)
    if(reset)
      state = 0;
    else
      state = state + 1;

  assert property (reset |-> ##1 state==0);
  assert property (reset |-> ##2 state==1);

endmodule

Now, run EBMC command to verify the counter circuit for a bound of ten as follows:

ebmc example4.sv --top counter --bound 10 --trace

The first assertion in the module checks that the reset signal correctly sets the value of the counter to zero. It passes. The second assertion in the module requires that the counter reaches the value one after two clock ticks after the reset cycle. Perhaps unexpectedly, this assertion fails. This is due to the fact that the reset signal is an input, and thus, may take arbitrary values. In particular, reset may be active in two consecutive time frames, which implies that the value of state will be zero, and not one, in the second time frame after the first reset.

We could, of course, write a harness for our module that initialises reset to one, and then sets it to zero in the next and any subsequent time frames. To save that effort, we can instruct EBMC to assume that the reset signal is driven in that fashion using the --reset command-line option. The design uses an active-high reset signal, so the reset expression is reset==1.

ebmc example4.sv --top counter --bound 10 --reset reset==1 

The second assertion now passes as well.