Detailed analysis of run-times is available in an accompanying Jupyter Notebook in Google Collab. We also contribute translations of the 2019/20 Hardware Model Checking Competion benchmarks to our Btor Dialect, LLVM-IR and SMT-LIB in hwmcc20-mlir. The image below shows the different verification strategies employed.
Consider a simple counter that ensures we do not reach 15, represented in Bᴛᴏʀ2 below:
1 sort bitvec 4
2 zero 1
3 state 1 out
4 init 1 3 2
5 one 1
6 add 1 3 5
7 next 1 3 6
8 ones 1
9 sort bitvec 1
10 eq 9 3 8
11 bad 10
Using the command build/bin/btor2mlir-translate --import-btor counter.btor2 > counter.mlir, where counter.btor2 is the file shown above, we get the equivalent representation of our circuit in the BTOR Dialect of MLIR below (counter.mlir):
module {
func @main() {
%0 = btor.constant 0 : i4 !btor.bv<4>
br ^bb1(%0 : !btor.bv<4>)
^bb1(%1: !btor.bv<4>): // 2 preds: ^bb0, ^bb1
%2 = btor.constant 1 : i4 !btor.bv<4>
%3 = btor.add %1, %2 : !btor.bv<4>
%4 = btor.constant -1 : i4 !btor.bv<4>
%5 = btor.cmp eq, %1, %4 : !btor.bv<4>
btor.assert_not(%5), 0 : i64 !btor.bv<1>
br ^bb1(%3 : !btor.bv<4>)
}
}Then, using the command build/bin/btor2mlir-opt --convert-std-to-llvm --convert-btor-to-llvm counter.mlir > counter.mlir.opt we get the file below which represents the original circuit in the LLVM Dialect of MLIR.
module attributes {llvm.data_layout = ""} {
llvm.func @__VERIFIER_error()
llvm.func @__VERIFIER_assert(i1, i64)
llvm.func @main() {
%0 = llvm.mlir.constant(0 : i4) : i4
llvm.br ^bb1(%0 : i4)
^bb1(%1: i4): // 2 preds: ^bb0, ^bb2
%2 = llvm.mlir.constant(1 : i4) : i4
%3 = llvm.add %1, %2 : i4
%4 = llvm.mlir.constant(-1 : i4) : i4
%5 = llvm.icmp "eq" %1, %4 : i4
%6 = llvm.mlir.constant(true) : i1
%7 = llvm.xor %5, %6 : i1
llvm.cond_br %7, ^bb2, ^bb3
^bb2: // pred: ^bb1
llvm.br ^bb1(%3 : i4)
^bb3: // pred: ^bb1
%8 = llvm.mlir.constant(0 : i64) : i64
llvm.call @__VERIFIER_assert(%7, %8) : (i1, i64) -> ()
llvm.call @__VERIFIER_error() : () -> ()
llvm.unreachable
}
}Finally, using the command build/bin/btor2mlir-translate --mlir-to-llvmir counter.mlir.opt > counter.ll we generate the circuit as an LLVM-IR program below (counter.ll):
declare void @__VERIFIER_error()
declare void @__VERIFIER_assert(i1, i64)
define void @main() !dbg !3 {
br label %1, !dbg !7
1: ; preds = %6, %0
%2 = phi i4 [ %3, %6 ], [ 0, %0 ]
%3 = add i4 %2, 1, !dbg !9
%4 = icmp eq i4 %2, -1, !dbg !10
%5 = xor i1 %4, true, !dbg !11
br i1 %5, label %6, label %7, !dbg !12
6: ; preds = %1
br label %1, !dbg !13
7: ; preds = %1
call void @__VERIFIER_assert(i1 %5, i64 0), !dbg !14
call void @__VERIFIER_error(), !dbg !15
unreachable, !dbg !16
}If you have SeaHorn installed locally (a distribution is included in the Docker), we can show that the bad state in the original circuit is reached using SeaHorn's Bounded Model Checking engine. This is indicated by the output sat when we run the command: sea bpf counter.ll
Run the shell script ./get_cex_seahorn.sh $btor2_file to:
a) extract a counter example from SeaHorn
b) generate a Btor2 Witness
c) simulate the witness using btorsim
Dockerfile: docker/btor2mlir.Dockerfile.
From the root folder use the following commands to:
Build: docker build -t btor2mlir . --file docker/btor2mlir.Dockerfile
Run: docker run -it btor2mlir
The instructions assume that cmake, clang/clang++ and ninja are installed on your machine, LLVM_PROJECT=/ag/llvm-gh-mlir, and that lit
command is installed and is globally available
Commands to configure and compile LLVM
$ mkdir debug && cd debug
$ cmake -G Ninja ../llvm \
-DCMAKE_C_COMPILER=clang-14 -DCMAKE_CXX_COMPILER=clang++-14 \
-DLLVM_ENABLE_PROJECTS=mlir -DLLVM_BUILD_EXAMPLES=ON \
-DCMAKE_BUILD_TYPE=Debug \ # change to RelWithDebInfo for release build
-DLLVM_TARGETS_TO_BUILD="X86" \
-DLLVM_ENABLE_LLD=ON \ # only on Linux
-DLLVM_INSTALL_UTILS=ON \ # optional to install FileCheck and lit
-DCMAKE_INSTALL_PREFIX=$(pwd)/run # install location in `run` under build
$ ninja
$ ninja installThe above installs a debug version of llvm under LLVM_PROJECT/debug/run,
where LLVM_PROJECT is the root of llvm project on your machine.
To compile this project
$ mkdir debug && cd debug
$ cmake -G Ninja .. \
-DMLIR_DIR=/ag/llvm-gh-mlir/debug/run/lib/cmake/mlir \
-DLLVM_DIR=/ag/llvm-gh-mlir/debug/run/lib/cmake/llvm \
-DLLVM_EXTERNAL_LIT=$(which lit) \
-DLLVM_ENABLE_LLD=ON \
-DCMAKE_INSTALL_PREFIX=$(pwd)/run \Arie Gurfinkel [email protected]
Joseph Tafese [email protected]
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent