f4069fa11e
Verilog: function/task ports |
||
---|---|---|
.github | ||
examples/fp_adder | ||
lib | ||
regression | ||
src | ||
.clang-format | ||
.gitmodules | ||
.travis.yml | ||
COMPILING.md | ||
LICENSE | ||
README.md |
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