Skip to content

diffblue/hw-cbmc

Folders and files

NameName
Last commit message
Last commit date
Dec 3, 2024
Nov 5, 2024
Jun 20, 2024
Dec 3, 2024
Nov 29, 2024
Dec 4, 2024
Dec 6, 2024
Nov 9, 2024
Nov 30, 2023
May 9, 2024
Jun 24, 2017
Sep 8, 2017
Dec 6, 2024
Dec 11, 2023
Jan 16, 2020
Oct 26, 2024

Repository files navigation

About

EBMC is a free, open-source formal verification tool for hardware designs. It can read Verilog 2005, SystemVerilog 2017, NuSMV and netlists (given in ISCAS89 format). Properties can be given in LTL or a fragment of SystemVerilog Assertions. It includes both bounded and (despite its name) unbounded Model Checking engines, i.e., it can both discover bugs and prove the absence of bugs.

For full information see cprover.org.

Usage

Let us assume we have the following SystemVerilog model in main.sv.

module main(input clk, x, y);

  reg [1:0] cnt1;
  reg z;

  initial cnt1=0;
  initial z=0;

  always @(posedge clk) cnt1=cnt1+1;

  always @(posedge clk)
    casex (cnt1)
      2'b00:;
      2'b01:;
      2'b1?: z=1;
    endcase

  p1: assert property (@(posedge clk) (z==0));

endmodule

We can then invoke the BMC engine in EBMC as follows:

$ ebmc main.sv --top main --bound 3

This sets the unwinding bound to 3 and the top-level module to main.

For more information see EBMC Manual.