diffblue / hw-cbmc Goto Github PK

The HW-CBMC and EBMC Model Checkers for Verilog

License: Other

Verilog 2.47% SystemVerilog 22.29% Makefile 0.84% Perl 0.09% C 4.45% VHDL 0.14% C++ 63.91% Shell 0.05% CMake 0.08% Yacc 4.58% Lex 1.09% Coq 0.01%

hw-cbmc's Introduction

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 SystemVerilog code 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

Then we can run the EBMC verification as

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

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

For more information see EBMC Manual

hw-cbmc's People

Contributors

Stargazers

Watchers

Forkers

mgudemann flians fanhy2114 tautschnig ruochendai78 crazybinaryli mrwater98 mhayat-10xe h-m-umar easyformal plutsyk abhinandan-pal kroening

hw-cbmc's Issues

Memory Exhaustion in SMV parser

With some of the benchmark files from https://www.cprover.org/ebmc/download/AIG_SMV_08.tar.gz

there is a memory exhausted error, e.g.

using default bound 1
Parsing AIG_SMV/dintel048.aig/intel048.aig.smv
file AIG_SMV/dintel048.aig/intel048.aig.smv line 271364: memory exhausted before 'a471304'

Inreasing YYMAXDEPTH in smvlang/parser.y for example to 2000000 fixes this at least for the above example.

segmentation fault on regression test

the regression test reset-command-line-option1 causes a segmentation fault on 8ed8c07 (when the --reset reset_n parameter is used, else it works)

EBMC/ic3 fails to verify property of `ring_buffer` example

both --bdd and --k-induction verify the property. Maybe --ic3 does not handle the assumes?

  wire full=count==15;
  wire empty=count==0;

  assume property (empty |-> !read);
  assume property (full |-> !write);

  assert property (((writeptr-readptr)&'b1111)==count);

use `satcheckt` solver in IC3

currently EBMC/ic3 uses a custom Minisat solver, this should become the satcheckt solver from CBMC.

Problems compiling current EBMC

Hi,
I tried building ebmc 975052e23a122438855ea37228db904dc3363c4d using gcc version 7.5.0 (Ubuntu 7.5.0-3ubuntu1~18.04)

There were two problems:

unused variable constraint causing an error because of the compiler settings in hw-cbmc/hw_cbmc_parse_options.cpp

  // the 'extra constraints'
  if (!constraints.empty()) {
    log.status() << "converting constraints" << messaget::eom;

    for (const auto &constraint : constraints) {
      // TODO : include the extra constraints using the new custom verifier
      // interface
    }
  }

this is easy to solve of course

undefined references for all the ID_XXX in hw_cbmc_irep_ids.h
for this I copied the contents of the file to CBMC's src/util/irep_ids.def

But my guess is that this is not the intended way to do this.
What I am missing?

PARSING ERROR syntax error before '__value' when verifying hardware of DUAL_PATH_ADDER of the FM16 paper's benchmark.

I encounter following error when trying hw-cbmc on the benchmarks of DUAL_PATH_ADDER (which is in http://www.cs.ox.ac.uk/people/rajdeep.mukherjee/FM16-experiments.tar.gz).

HW-CBMC version 5.94.0 (cbmc-5.94.0-dirty)
Starting Bounded Model Checking
Parsing fp_comparison.c
file /usr/include/x86_64-linux-gnu/bits/mathcalls-helper-functions.h line 20: syntax error before '__value'
PARSING ERROR

the command is

time ~/hw-cbmc/src/hw-cbmc/hw-cbmc fp_comparison.c fp_adder.v --module fp_add_sub --bound 1 hw_cbmc_harness.c

This error report seems to be similar to #2152 if cbmc, but I use new version of cbmc and hw-cbmc.

I am using Ubuntu 22.04, and

/usr/include/x86_64-linux-gnu/bits/mathcalls-helper-functions.h

/* Prototype declarations for math classification macros helpers.
   Copyright (C) 2017-2022 Free Software Foundation, Inc.
   This file is part of the GNU C Library.

   The GNU C Library is free software; you can redistribute it and/or
   modify it under the terms of the GNU Lesser General Public
   License as published by the Free Software Foundation; either
   version 2.1 of the License, or (at your option) any later version.

   The GNU C Library is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   Lesser General Public License for more details.

   You should have received a copy of the GNU Lesser General Public
   License along with the GNU C Library; if not, see
   <https://www.gnu.org/licenses/>.  */

/* Classify given number.  */
__MATHDECL_ALIAS (int, __fpclassify,, (_Mdouble_ __value), fpclassify)
     __attribute__ ((__const__));

/* Test for negative number.  */
__MATHDECL_ALIAS (int, __signbit,, (_Mdouble_ __value), signbit)
     __attribute__ ((__const__));

/* Return 0 if VALUE is finite or NaN, +1 if it
   is +Infinity, -1 if it is -Infinity.  */
__MATHDECL_ALIAS (int, __isinf,, (_Mdouble_ __value), isinf)
  __attribute__ ((__const__));

/* Return nonzero if VALUE is finite and not NaN.  Used by isfinite macro.  */
__MATHDECL_ALIAS (int, __finite,, (_Mdouble_ __value), finite)
  __attribute__ ((__const__));

/* Return nonzero if VALUE is not a number.  */
__MATHDECL_ALIAS (int, __isnan,, (_Mdouble_ __value), isnan)
  __attribute__ ((__const__));

/* Test equality.  */
__MATHDECL_ALIAS (int, __iseqsig,, (_Mdouble_ __x, _Mdouble_ __y), iseqsig);

/* Test for signaling NaN.  */
__MATHDECL_ALIAS (int, __issignaling,, (_Mdouble_ __value), issignaling)
     __attribute__ ((__const__));

Verilog Parser 4.4 has problems with file

in this (https://groups.google.com/forum/#!topic/cprover-support/rQrlv7NY79A)[thread] a user posted a Verilog file for which apparently properties can only be specified on the command line, properties in the file give

        file or1200_if.v line 222: syntax error before ' ( '
        PARSING ERROR

version 4.4 fails even when the property is specified on the command line

Parsing or1200_if.v
Converting
Type-checking Verilog::or1200_if
Type-checking Verilog::main
--- begin invariant violation report ---
Invariant check failed
File ../../lib/cbmc/src/util/message.h function get_message_handler line 129
Reason: message handler is setBacktrace:
Backtrace
ebmc() [0x46e191]
ebmc() [0x46e706]
ebmc() [0x42ccbd]
ebmc() [0x42cc8b]
ebmc() [0x42a868]
ebmc() [0x5f3ea4]
ebmc() [0x42add0]
ebmc() [0x4267de]
ebmc() [0x4299ba]
ebmc() [0x4441ad]
ebmc() [0x417ca2]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf0) [0x7f25b62b6830]
ebmc() [0x40c2a9]


--- end invariant violation report ---
fish: “ebmc  or1200_if.v --module main…” terminated by signal SIGABRT (Abort)

which works with 4.2

Parser exhausts memory on large SMV files (converted from AIG)

on the attached .smv from AIG_SMV_08 benchmark, ebmc 4.2 and current 4.4 fail with

Parsing intel048.aig.smv
file intel048.aig.smv line 271364: memory exhausted before `a471304'
PARSING ERROR

due to bison exhausting its memory

Assertion violation `Assertion `!isEliminated(v)' failed.` in 4.4

For the attached model, --bound 12 should falsify smv::main::spec1, but results in

ebmc-4.4: ../../minisat-2.2.1/minisat/simp/SimpSolver.cc:106: Minisat::lbool Minisat::SimpSolver::solve_(bool, bool): Assertion `!isEliminated(v)' failed.
fish: “~/source/formal_methods/ebmc-4.…” terminated by signal SIGABRT (Abort)

elbtunnel.zip

real PO values (with CEX depth):

PO 0 - k: ..........no([0])
PO 1 - k: .yes([1])
PO 2 - k: ....no([2])
PO 3 - k: .........no([3])
PO 4 - k: .yes([4])
PO 5 - k: ........yes([5])
PO 6 - k: ..........no([6])
PO 7 - k: ..........no([7])

Could not parse macro in verilog file

Encountered errors while parsing using EBMC: unknown preprocessor macro "SR_SMODE_MASK".

regression test `SVA_LTL1` fails

EBMC fails to read SMV files with `.` in name

for example the attached smv model fails with

Parsing counter.aig.smv
file counter.aig.smv line 2: syntax error before `9'
PARSING ERROR

on both 4.4. and 4.2
counter.zip

issue in implication operator

When I execute example3.sv, which was given by EBMC, it gives me the error 'file example3.sv line 14: syntax error before `|->' PARSING ERROR'. Are implication operators supported in EBMC, or is there any other mistake I am making?

ic3: property numbers

The 'short_name' idea seems to be that properties end on a dot followed by a unique number. This is not the case.

Instead of --prop, please use --property, to be consistent with the rest of ebmc.

BDD2/3/5 regression tests fail

BDD2 takes huge amounts of RAM >80% for 16G
BDD3 and BDD5 fail to match test.desc

Invariant Violation Report

I tried to verify a simple design in vcegar-benchmarks, but I encountered the following error message.

hw-cbmc version: main-lastest
Verilog code:

module main (clk);
input clk;
reg [2500:0] a,b;	
	
initial a = 1;
initial b = 0;

always @ (posedge clock) begin
	if (a<100) 
	   a<=b+a;
	b <=a;
end

endmodule

ebmc command:

ebmc example.v --top main --bound 10 -p "a < 200"

error messag:

Parsing example.v
Converting
Type-checking Verilog::main
file example.v line 9: implicit wire main.clock
--- begin invariant violation report ---
Invariant check failed
File: ../../lib/cbmc/src/util/message.h:188 function: get_message_handler
Condition: message_handler!=nullptr
Reason: message handler should be set before calling get_message_handler
Backtrace:
0   ebmc                                0x000000010e3fcfea _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   ebmc                                0x000000010e3fd587 _Z13get_backtracev + 183
2   ebmc                                0x000000010e4b19fc _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 44
3   ebmc                                0x000000010e4b19c9 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 9
4   ebmc                                0x000000010e648643 _ZN8messaget19get_message_handlerEv + 115
5   ebmc                                0x000000010e5f5f5f _ZN17verilog_languaget7to_exprERKNSt3__112basic_stringIcNS0_11char_traitsIcEENS0_9allocatorIcEEEES8_R5exprtRK10namespacet + 175
6   ebmc                                0x000000010e659c28 _ZN16ebmc_propertiest17from_command_lineERK8cmdlinetRK18transition_systemtR16message_handlert + 200
7   ebmc                                0x000000010e654eab _ZN10ebmc_baset14get_propertiesEv + 59
8   ebmc                                0x000000010e657f81 _ZN19ebmc_parse_optionst4doitEv + 3105
9   ebmc                                0x000000010e42891c _ZN19parse_options_baset4mainEv + 140
10  ebmc                                0x000000010e65ead8 main + 40
11  dyld                                0x00007ff81ca2a41f start + 1903


--- end invariant violation report ---
[1]    7888 abort      ebmc example.v --top main --bound 10 -p "a < 200"

However, if I write the property that needs to be verified directly in the Verilog file, it just works.
Verilog code:

module main (clk);
input clk;
reg [2500:0] a,b;	
	
initial a = 1;
initial b = 0;

always @ (posedge clock) begin
	if (a<100) 
	   a<=b+a;
	b <=a;
end

always begin
assert property: (a<200);
end

endmodule

ebmc command:

ebmc example.v --top main --bound 20

Is this expected behavior? And do I misunderstand how to use ebmc?

mv: cannot stat 'y.tab.cpp.h': No such file or directory

Hi,
I tried building ebmc 975052e using cd src; make command.
There are a problem:
if [ -e verilog_y.tab.hpp ] ; then mv verilog_y.tab.hpp verilog_y.tab.h ; else \ mv y.tab.cpp.h y.tab.h ; fi mv: cannot stat 'y.tab.cpp.h': No such file or directory make[1]: *** [Makefile:30: verilog_y.tab.h] Error 1

Implement circuit reduction

find / eliminate equivalent latches (or negation-equivalent ones)
reduction of combinatorial nodes
find implications

While SAT simplification can reduce the query size a help a lot, already creating smaller circuit representations / netlists has shown to be very beneficial in addition. For IC3 reducing the number of latches leads to smaller cubes, for induction/BMC all reductions are beneficial, either by reducing the circuit or by strengthening the properties. Finding implications might only be beneficial for induction/BMC.

EBMC/ic3 fails to analyze SMV converted from AIG

on master seems to be stuck at this

Parsing ./dpdtvisns3p02.aig/pdtvisns3p02.aig.smv
Converting
Type-checking smv::main
Generating Netlist

again, example from AIG_SMV_08

segfault on typecheck

For some of the SMV models converted from Aiger format, EBMC fails with sefgault which typechecking.
The example is from http://www.cprover.org/ebmc/download/AIG_SMV_08.tar.gz

aig.zip

EBMC 4.4 fails to analyze VHDL regression tests

fails with

~/source/formal_methods/ebmc-4.4 boolean1.vhd 
Parsing boolean1.vhd
Converting
Type-checking boolean1_test
symbol `true' not found
CONVERSION ERROR

and

~/source/formal_methods/ebmc-4.4 std_logic1.vhd 
Parsing std_logic1.vhd
Converting
Type-checking std_logic1_test
unknown type `std_logic'
CONVERSION ERROR

Solving time problem

When verifying a Verilog design using ebmc with large bounds, it takes long time to complete the verification. However, if I output the SMT formulas and solve the formulas using z3 command, it takes instant to solve the problem. In my opinion, these two approaches should consume similar time since encoding Verilog and properties as SMT formulas is fast. Here's the procedure to reproduce the phenomenon.

hw-cbmc version: main-latest

Verilog code:

module main (clk);
input clk;
reg [2500:0] a,b;	
	
initial a = 1;
initial b = 0;

always @ (posedge clock) begin
	if (a<100) 
	   a<=b+a;
	b <=a;
end

endmodule

ebmc verification command:

ebmc example.v --top main --bound 1000 -p "a < 200" --z3

This command takes almost 110 seconds on my machine.

ebmc export SMT formula:

ebmc example.v --top main --bound 1000 -p "a < 200" --smt2 | awk '!/^Parsing|^Converting|^Type-checking|^Generating|^Properties/ END {print "(check-sat)"}' > formula.smt

This command exports formulas in SMT lib 2 format. Then I tried to solve the formulas with z3:

z3 -model -smt2 formula.smt -st

And it outputs the following instantly:

unsat
(:max-memory   21.89
 :memory       20.90
 :num-allocs   2516964
 :rlimit-count 56060
 :time         0.01
 :total-time   0.04)

In model checking approach, unsat means that the property is proved up to the bound, right? So, my question is that why the time consumptions of these two approaches differ so greatly?

questions about co-verification tool HW-CBMC supporting for concurrency scenarios

can the co-verification tool HW-CBMC support for CPU and DMA device concurrency scenario, for example, to verify the Memory Consistency or resources race?

Setup CBMC as git submodule for HW-CBMC

Analogously to CBMC in test-gen, we should set-up CBMC as git submodule for HW-CBMC, in order to make it easier to compile using a specific CBMC commit.