Go to file
Michael Tautschnig f4069fa11e
Merge pull request #334 from diffblue/function_ports1
Verilog: function/task ports
2024-02-07 17:49:21 +01:00
.github CI: run the Verilog tests with Z3 2024-02-03 08:22:27 -08:00
examples/fp_adder adder harness 2014-09-29 12:38:22 +00:00
lib bump cbmc dependency 2024-01-06 11:11:36 -08:00
regression Verilog: function/task ports 2024-02-05 06:15:04 -08:00
src Merge pull request #334 from diffblue/function_ports1 2024-02-07 17:49:21 +01:00
.clang-format Add clang-format GitHub action 2023-11-30 09:59:41 +00:00
.gitmodules Add CBMC as git submodule for HW-CBMC 2017-06-24 16:49:17 +02:00
.travis.yml enable Travis CI 2017-09-08 11:48:17 +01:00
COMPILING.md ebmc: move compilation instructions into COMPILING.md 2023-12-11 03:58:08 -08:00
LICENSE Add proper BSD 3 clause LICENSE file 2020-01-16 15:58:38 +00:00
README.md ebmc: move compilation instructions into COMPILING.md 2023-12-11 03:58:08 -08:00

README.md

About

EBMC is a bounded model checker for the Verilog language (and other HW specification languages). The verification is performed by synthesizing a transition system from the Verilog, unwinding the transition system (up to a certain bound), and then producing a decision problem. The decision problem encodes the circuit and the negation of the property under verification. Hence if satisfiable, the tool produces a counterexample demonstrating violation of the property. EBMC can use CBMC's bit-vector solver or Z3 or CVC4 to solve the decision problem.

For full information see cprover.org.

Usage

Let us assume we have the following Verilog code in main.v.


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

  always assert p1: z==0;

endmodule

Then we can run the EBMC verification as

$> ebmc main.v --module main --bound 3

setting the unwinding bound to 3 and running the verification of the module main.

For more information see EBMC Manual