BMC: a word level model checker base on smt-switch

BMC is an extensible SMT-based model checker implemented in C++. There are some new features compared with the normal BMC(Bound Model Checking).

• can do inverse bmc which start at bad state
• skip steps to reduce the call of SMT-solver (e.g. check bound 1,3,5,7...)
• parallel bmc, doing skip bmc by mutithreads makes bmc parallel.

Setup

1. git clone https://github.com/donghua100/bmc.git clone the bmc project
2. cd bmc
3. mkdir deps && cd deps create deps directory and build smt-swith and btor2tools in it.

Build smt-switch

make sure you are in deps.

git clone https://github.com/stanford-centaur/smt-switch.git
# build Boolector, cvc5, z3 solver use scripts.
./contrib/setup-btor.sh
./contrib/setup-cvc5.sh
./contrib/setup-z3.sh
# Note: build yices2 Mathsat 5
# you should  build yices2 Mathsat 5 manually flowing smt-switch readme
# then
./configure.sh --btor --cvc5 --msat --yices2 --z3 --static
cd build
make -j$(nproc)

Build Btor2tools

make sure you are in deps.

git clone https://github.com/Boolector/btor2tools.git
./configure.sh
cd build
make

4. in bmc project directory, mkdir build && cd build && cmake .. && make Build BMC.

How to Use

For system verilog we privide the template of yosys scripts, which can be found in yosys. First ues Yosys convert system verilog to btor format.

# this command will generate btor file for myconter-false.v, which is a counter. 
yosys yosys/conter-false.ys

./bmc <path>/<file>.btor
Example:					 ./bmc ../tset/counter-false.btor

Here is output

start bmc..
Checking steps at 1
Checking step 1 takes time: 0 sec
Checking steps at 2
Checking step 2 takes time: 0 sec
Checking steps at 3
Checking step 3 takes time: 0 sec
Checking steps at 4
Checking step 4 takes time: 0 sec
find counter-example
sat
b0
#0
0 00000000000000000000000000000000 cnt@0
1 0 state8@0
2 0 state10@0
@0
0 0 clk@0
@1
0 0 clk@1
@2
0 0 clk@2
@3
0 0 clk@3
@4
0 0 clk@4
.
Trace written to dump.vcd

If the conterexample if found, vcd file will be generated.Here is the vcd file generated by execute example command.