llvm
export to smtlib
Hello, I am attempting to export a Verilog file to smtlib and am receiving errors or an empty file. Could someone clarify how complete the functionality is or what the pipeline formats are for conversion?
P.S. I am also trying to figure out how to get the verif dialect, since I am unable to do so.
Hi @Ckaf!
We don't really have a path from Verilog to a generically usable SMTLIB output currently - the reason for this is that our flow from hardware to SMTLIB targets model checking, so the IR node that actually indicates we add an SMTLIB assertion is an assertion in the IR (since anything that isn't in the fan-in to an assertion can be ignored for model-checking - this is probably why you were seeing empty files).
As a temporary workaround, it should work to try adding some arbitrary assertion on the output of your module and running that through the lowerings to SMT - that should produce some SMTLIB which calculates the output of your module and applies that assertion against it. Note that this will only work with a purely combinational module (due to the complications of representing state in SMTLIB).
In the long-run it would definitely be nice to have a way to emit SMTLIB corresponding to hardware without requiring an assertion - having discussed this with @maerhart, the best way to do this is probably with a modification to the HWToSMT pass that declares constants that correspond to the module outputs. I'll add this to my todo list, and I'll drop another comment here if I get the time to put something together!
Hey @Ckaf! I've pushed a couple of PRs this week that mean we now have a flow for converting combinational modules to usable SMTLIB. If you add the for-smtlib-export to your HWToSMT call in whatever flow you were using (syntactically set as circt-opt --hw-to-smt='for-smtlib-export'), that should in theory give you an smt.solver op that you can give to circt-translate --export-smtlib and get out some SMTLIB that represents your design. Note that this won't work if there's any module hierarchy, but you can run --hw-flatten-modules at the start of your flow to squash hierarchies into a single module.
Hopefully that's the missing piece you need, but let me know if not and we can take a look at what's missing to get you a working flow!
Hello @TaoBi22! That's great! I am currently researching open tools for formal verification of hardware circuits, and I am interested in what the current limitations are for supporting circuits with internal states. Is it simply a lack of manpower, or is there a deeper problem? Can I help in any way, and does anyone have a general vision?
P.S. I noticed this while compiling the project.
FAILED: [code=1] tools/circt/lib/Transforms/CMakeFiles/obj.CIRCTTransforms.dir/FlattenMemRefs.cpp.o
/usr/bin/c++ -DCIRCT_INCLUDE_TESTS -DGTEST_HAS_RTTI=0 -D_DEBUG -D_GLIBCXX_ASSERTIONS -D_GLIBCXX_USE_CXX11_ABI=1 -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -I/home/ckaf/circt/build/tools/circt/lib/Transforms -I/home/ckaf/circt/lib/Transforms -I/home/ckaf/circt/build/include -I/home/ckaf/circt/llvm/llvm/include -I/home/ckaf/circt/include -I/home/ckaf/circt/build/tools/circt/include -isystem /home/ckaf/circt/llvm/llvm/../mlir/include -isystem /home/ckaf/circt/build/tools/mlir/include -fPIC -fno-semantic-interposition -fvisibility-inlines-hidden -Werror=date-time -Wall -Wextra -Wno-unused-parameter -Wwrite-strings -Wcast-qual -Wno-missing-field-initializers -pedantic -Wno-long-long -Wimplicit-fallthrough -Wno-maybe-uninitialized -Wno-nonnull -Wno-class-memaccess -Wno-dangling-reference -Wno-redundant-move -Wno-pessimizing-move -Wno-array-bounds -Wno-stringop-overread -Wno-noexcept-type -Wdelete-non-virtual-dtor -Wsuggest-override -Wno-comment -Wno-misleading-indentation -Wctad-maybe-unsupported -fdiagnostics-color -ffunction-sections -fdata-sections -O2 -g -DNDEBUG -std=c++17 -fvisibility-inlines-hidden -fno-exceptions -funwind-tables -fno-rtti -UNDEBUG -gsplit-dwarf -MD -MT tools/circt/lib/Transforms/CMakeFiles/obj.CIRCTTransforms.dir/FlattenMemRefs.cpp.o -MF tools/circt/lib/Transforms/CMakeFiles/obj.CIRCTTransforms.dir/FlattenMemRefs.cpp.o.d -o tools/circt/lib/Transforms/CMakeFiles/obj.CIRCTTransforms.dir/FlattenMemRefs.cpp.o -c /home/ckaf/circt/lib/Transforms/FlattenMemRefs.cpp
/home/ckaf/circt/lib/Transforms/FlattenMemRefs.cpp:19:10: fatal error: mlir/Dialect/ControlFlow/Transforms/StructuralTypeConversions.h: No such file or directory
19 | #include "mlir/Dialect/ControlFlow/Transforms/StructuralTypeConversions.h"
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
compilation terminated.
Okay, I was able to compile the project. The issue was with the flag -DLLVM_ENABLE_LLD=ON, and I think I can even fix it if I get around to it.
I tried to do as you described and got an error. I will attach the input format for clarity.
➜ smt_check circt-opt --convert-hw-to-smt='for-smtlib-export' results/alu.hw.mlir
module {
smt.solver() : () -> () {
%0 = smt.declare_fun : !smt.bv<8>
%1 = builtin.unrealized_conversion_cast %0 : !smt.bv<8> to i8
%2 = smt.declare_fun : !smt.bv<8>
%3 = builtin.unrealized_conversion_cast %2 : !smt.bv<8> to i8
%4 = smt.declare_fun : !smt.bv<3>
%5 = builtin.unrealized_conversion_cast %4 : !smt.bv<3> to i3
%c0_bv7 = smt.bv.constant #smt.bv<0> : !smt.bv<7>
%6 = builtin.unrealized_conversion_cast %c0_bv7 : !smt.bv<7> to i7
%c-1_bv1 = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
%7 = builtin.unrealized_conversion_cast %c-1_bv1 : !smt.bv<1> to i1
%c0_bv8 = smt.bv.constant #smt.bv<0> : !smt.bv<8>
%8 = builtin.unrealized_conversion_cast %c0_bv8 : !smt.bv<8> to i8
%c-2_bv3 = smt.bv.constant #smt.bv<-2> : !smt.bv<3>
%9 = builtin.unrealized_conversion_cast %c-2_bv3 : !smt.bv<3> to i3
%c-3_bv3 = smt.bv.constant #smt.bv<-3> : !smt.bv<3>
%10 = builtin.unrealized_conversion_cast %c-3_bv3 : !smt.bv<3> to i3
%c-4_bv3 = smt.bv.constant #smt.bv<-4> : !smt.bv<3>
%11 = builtin.unrealized_conversion_cast %c-4_bv3 : !smt.bv<3> to i3
%c3_bv3 = smt.bv.constant #smt.bv<3> : !smt.bv<3>
%12 = builtin.unrealized_conversion_cast %c3_bv3 : !smt.bv<3> to i3
%c0_bv1 = smt.bv.constant #smt.bv<0> : !smt.bv<1>
%13 = builtin.unrealized_conversion_cast %c0_bv1 : !smt.bv<1> to i1
%c2_bv3 = smt.bv.constant #smt.bv<2> : !smt.bv<3>
%14 = builtin.unrealized_conversion_cast %c2_bv3 : !smt.bv<3> to i3
%c1_bv3 = smt.bv.constant #smt.bv<1> : !smt.bv<3>
%15 = builtin.unrealized_conversion_cast %c1_bv3 : !smt.bv<3> to i3
%c0_bv3 = smt.bv.constant #smt.bv<0> : !smt.bv<3>
%16 = builtin.unrealized_conversion_cast %c0_bv3 : !smt.bv<3> to i3
%17 = comb.icmp ceq %5, %16 : i3
%18 = comb.concat %13, %1 : i1, i8
%19 = comb.concat %13, %3 : i1, i8
%20 = comb.add %18, %19 : i9
%21 = comb.extract %20 from 8 : (i9) -> i1
%22 = comb.extract %20 from 0 : (i9) -> i8
%23 = comb.icmp ceq %5, %15 : i3
%24 = comb.sub %18, %19 : i9
%25 = comb.extract %24 from 8 : (i9) -> i1
%26 = comb.extract %24 from 0 : (i9) -> i8
%27 = comb.icmp ceq %5, %14 : i3
%28 = comb.and %1, %3 : i8
%29 = comb.icmp ceq %5, %12 : i3
%30 = comb.or %1, %3 : i8
%31 = comb.icmp ceq %5, %11 : i3
%32 = comb.xor %1, %3 : i8
%33 = comb.icmp ceq %5, %10 : i3
%34 = comb.extract %1 from 0 : (i8) -> i7
%35 = comb.concat %34, %13 : i7, i1
%36 = comb.extract %1 from 7 : (i8) -> i1
%37 = comb.extract %1 from 1 : (i8) -> i7
%38 = comb.concat %13, %37 : i1, i7
%39 = comb.icmp eq %1, %3 : i8
%40 = comb.concat %6, %39 : i7, i1
%41 = comb.xor %17, %7 : i1
%42 = comb.xor %23, %7 : i1
%43 = comb.and %42, %41 : i1
%44 = comb.xor %27, %7 : i1
%45 = comb.and %44, %43 : i1
%46 = comb.xor %29, %7 : i1
%47 = comb.and %46, %45 : i1
%48 = comb.xor %31, %7 : i1
%49 = comb.and %48, %47 : i1
%50 = comb.and %33, %49 : i1
%51 = comb.mux %50, %35, %38 : i8
%52 = comb.and %31, %47 : i1
%53 = comb.xor %52, %7 : i1
%54 = comb.mux %52, %32, %51 : i8
%55 = comb.and %29, %45 : i1
%56 = comb.xor %55, %7 : i1
%57 = comb.mux %55, %30, %54 : i8
%58 = comb.and %27, %43 : i1
%59 = comb.xor %58, %7 : i1
%60 = comb.and %59, %56, %53, %50, %36 : i1
%61 = comb.mux %58, %28, %57 : i8
%62 = comb.and %23, %41 : i1
%63 = comb.mux %62, %25, %60 : i1
%64 = comb.mux %62, %26, %61 : i8
%65 = comb.mux %17, %21, %63 : i1
%66 = comb.mux %17, %22, %64 : i8
%67 = comb.xor %33, %7 : i1
%68 = comb.icmp cne %5, %9 : i3
%69 = comb.and %68, %67, %49 : i1
%70 = comb.xor %69, %7 : i1
%71 = comb.and %70, %65 : i1
%72 = builtin.unrealized_conversion_cast %71 : i1 to !smt.bv<1>
%73 = comb.mux %69, %40, %66 : i8
%74 = builtin.unrealized_conversion_cast %73 : i8 to !smt.bv<8>
%75 = comb.icmp eq %73, %8 : i8
%76 = builtin.unrealized_conversion_cast %75 : i1 to !smt.bv<1>
%77 = smt.declare_fun : !smt.bv<8>
%78 = smt.eq %74, %77 : !smt.bv<8>
smt.assert %78
%79 = smt.declare_fun : !smt.bv<1>
%80 = smt.eq %72, %79 : !smt.bv<1>
smt.assert %80
%81 = smt.declare_fun : !smt.bv<1>
%82 = smt.eq %76, %81 : !smt.bv<1>
smt.assert %82
}
}
➜ smt_check circt-opt --convert-hw-to-smt='for-smtlib-export' results/alu.hw.mlir -o results/alu.smt_generated_from_hw.mlir
➜ smt_check circt-translate --export-smtlib results/alu.smt_generated_from_hw.mlir
results/alu.smt_generated_from_hw.mlir:31:11: error: Dialect `comb' not found for custom op 'comb.icmp'
%17 = comb.icmp ceq %5, %16 : i3
^
results/alu.smt_generated_from_hw.mlir:31:11: note: Available dialects: arith, builtin, func, smt ; for more info on dialect registration see https://mlir.llvm.org/getting_started/Faq/#registered-loaded-dependent-whats-up-with-dialects-management
Hello @TaoBi22! That's great! I am currently researching open tools for formal verification of hardware circuits, and I am interested in what the current limitations are for supporting circuits with internal states. Is it simply a lack of manpower, or is there a deeper problem? Can I help in any way, and does anyone have a general vision?
Representing stateful circuits in SMTLIB is fundamentally non-trivial since SMTLIB has no concept of state/procedure/time (i.e., there's not really a clear way to represent a register in SMTLIB). Bounded model checkers tend to handle the issue by building a new set of constraints in the SMT problem for each cycle, and invoking the SMT/SAT solver on each cycle (or by combining all the unrolled states into one invocation).
There are some ways to encode things like reachability in SMTLIB though, using e.g. Constrained Horn Clauses, so you can check a bad state isn't reachable. Do you have a specific use-case in mind?
Okay, I was able to compile the project. The issue was with the flag
-DLLVM_ENABLE_LLD=ON, and I think I can even fix it if I get around to it.I tried to do as you described and got an error. I will attach the input format for clarity.
➜ smt_check circt-opt --convert-hw-to-smt='for-smtlib-export' results/alu.hw.mlir module { smt.solver() : () -> () { %0 = smt.declare_fun : !smt.bv<8> %1 = builtin.unrealized_conversion_cast %0 : !smt.bv<8> to i8 %2 = smt.declare_fun : !smt.bv<8> %3 = builtin.unrealized_conversion_cast %2 : !smt.bv<8> to i8 %4 = smt.declare_fun : !smt.bv<3> %5 = builtin.unrealized_conversion_cast %4 : !smt.bv<3> to i3 %c0_bv7 = smt.bv.constant #smt.bv<0> : !smt.bv<7> %6 = builtin.unrealized_conversion_cast %c0_bv7 : !smt.bv<7> to i7 %c-1_bv1 = smt.bv.constant #smt.bv<-1> : !smt.bv<1> %7 = builtin.unrealized_conversion_cast %c-1_bv1 : !smt.bv<1> to i1 %c0_bv8 = smt.bv.constant #smt.bv<0> : !smt.bv<8> %8 = builtin.unrealized_conversion_cast %c0_bv8 : !smt.bv<8> to i8 %c-2_bv3 = smt.bv.constant #smt.bv<-2> : !smt.bv<3> %9 = builtin.unrealized_conversion_cast %c-2_bv3 : !smt.bv<3> to i3 %c-3_bv3 = smt.bv.constant #smt.bv<-3> : !smt.bv<3> %10 = builtin.unrealized_conversion_cast %c-3_bv3 : !smt.bv<3> to i3 %c-4_bv3 = smt.bv.constant #smt.bv<-4> : !smt.bv<3> %11 = builtin.unrealized_conversion_cast %c-4_bv3 : !smt.bv<3> to i3 %c3_bv3 = smt.bv.constant #smt.bv<3> : !smt.bv<3> %12 = builtin.unrealized_conversion_cast %c3_bv3 : !smt.bv<3> to i3 %c0_bv1 = smt.bv.constant #smt.bv<0> : !smt.bv<1> %13 = builtin.unrealized_conversion_cast %c0_bv1 : !smt.bv<1> to i1 %c2_bv3 = smt.bv.constant #smt.bv<2> : !smt.bv<3> %14 = builtin.unrealized_conversion_cast %c2_bv3 : !smt.bv<3> to i3 %c1_bv3 = smt.bv.constant #smt.bv<1> : !smt.bv<3> %15 = builtin.unrealized_conversion_cast %c1_bv3 : !smt.bv<3> to i3 %c0_bv3 = smt.bv.constant #smt.bv<0> : !smt.bv<3> %16 = builtin.unrealized_conversion_cast %c0_bv3 : !smt.bv<3> to i3 %17 = comb.icmp ceq %5, %16 : i3 %18 = comb.concat %13, %1 : i1, i8 %19 = comb.concat %13, %3 : i1, i8 %20 = comb.add %18, %19 : i9 %21 = comb.extract %20 from 8 : (i9) -> i1 %22 = comb.extract %20 from 0 : (i9) -> i8 %23 = comb.icmp ceq %5, %15 : i3 %24 = comb.sub %18, %19 : i9 %25 = comb.extract %24 from 8 : (i9) -> i1 %26 = comb.extract %24 from 0 : (i9) -> i8 %27 = comb.icmp ceq %5, %14 : i3 %28 = comb.and %1, %3 : i8 %29 = comb.icmp ceq %5, %12 : i3 %30 = comb.or %1, %3 : i8 %31 = comb.icmp ceq %5, %11 : i3 %32 = comb.xor %1, %3 : i8 %33 = comb.icmp ceq %5, %10 : i3 %34 = comb.extract %1 from 0 : (i8) -> i7 %35 = comb.concat %34, %13 : i7, i1 %36 = comb.extract %1 from 7 : (i8) -> i1 %37 = comb.extract %1 from 1 : (i8) -> i7 %38 = comb.concat %13, %37 : i1, i7 %39 = comb.icmp eq %1, %3 : i8 %40 = comb.concat %6, %39 : i7, i1 %41 = comb.xor %17, %7 : i1 %42 = comb.xor %23, %7 : i1 %43 = comb.and %42, %41 : i1 %44 = comb.xor %27, %7 : i1 %45 = comb.and %44, %43 : i1 %46 = comb.xor %29, %7 : i1 %47 = comb.and %46, %45 : i1 %48 = comb.xor %31, %7 : i1 %49 = comb.and %48, %47 : i1 %50 = comb.and %33, %49 : i1 %51 = comb.mux %50, %35, %38 : i8 %52 = comb.and %31, %47 : i1 %53 = comb.xor %52, %7 : i1 %54 = comb.mux %52, %32, %51 : i8 %55 = comb.and %29, %45 : i1 %56 = comb.xor %55, %7 : i1 %57 = comb.mux %55, %30, %54 : i8 %58 = comb.and %27, %43 : i1 %59 = comb.xor %58, %7 : i1 %60 = comb.and %59, %56, %53, %50, %36 : i1 %61 = comb.mux %58, %28, %57 : i8 %62 = comb.and %23, %41 : i1 %63 = comb.mux %62, %25, %60 : i1 %64 = comb.mux %62, %26, %61 : i8 %65 = comb.mux %17, %21, %63 : i1 %66 = comb.mux %17, %22, %64 : i8 %67 = comb.xor %33, %7 : i1 %68 = comb.icmp cne %5, %9 : i3 %69 = comb.and %68, %67, %49 : i1 %70 = comb.xor %69, %7 : i1 %71 = comb.and %70, %65 : i1 %72 = builtin.unrealized_conversion_cast %71 : i1 to !smt.bv<1> %73 = comb.mux %69, %40, %66 : i8 %74 = builtin.unrealized_conversion_cast %73 : i8 to !smt.bv<8> %75 = comb.icmp eq %73, %8 : i8 %76 = builtin.unrealized_conversion_cast %75 : i1 to !smt.bv<1> %77 = smt.declare_fun : !smt.bv<8> %78 = smt.eq %74, %77 : !smt.bv<8> smt.assert %78 %79 = smt.declare_fun : !smt.bv<1> %80 = smt.eq %72, %79 : !smt.bv<1> smt.assert %80 %81 = smt.declare_fun : !smt.bv<1> %82 = smt.eq %76, %81 : !smt.bv<1> smt.assert %82 } } ➜ smt_check circt-opt --convert-hw-to-smt='for-smtlib-export' results/alu.hw.mlir -o results/alu.smt_generated_from_hw.mlir ➜ smt_check circt-translate --export-smtlib results/alu.smt_generated_from_hw.mlir results/alu.smt_generated_from_hw.mlir:31:11: error: Dialect `comb' not found for custom op 'comb.icmp' %17 = comb.icmp ceq %5, %16 : i3 ^ results/alu.smt_generated_from_hw.mlir:31:11: note: Available dialects: arith, builtin, func, smt ; for more info on dialect registration see https://mlir.llvm.org/getting_started/Faq/#registered-loaded-dependent-whats-up-with-dialects-management
Ah, the issue here is that you've converted your hw ops into the SMT dialect, but your operations from the comb dialect still need to be converted - you'll need to add --convert-comb-to-smt in the sequence of passes you run
I think that's what I need, but I still can't get it to work.
➜ smt_check circt-opt --convert-comb-to-smt results/alu.hw.mlir
results/alu.hw.mlir:14:10: error: failed to legalize operation 'comb.icmp' that was explicitly marked illegal
%0 = comb.icmp ceq %op, %c0_i3 : i3
^
results/alu.hw.mlir:14:10: note: see current operation: %22 = "comb.icmp"(<<UNKNOWN SSA VALUE>>, %21) <{predicate = 10 : i64}> : (i3, i3) -> i1
➜ smt_check circt-opt --convert-comb-to-smt results/alu.smt_generated_from_hw.mlir
results/alu.smt_generated_from_hw.mlir:31:11: error: failed to legalize operation 'comb.icmp' that was explicitly marked illegal
%17 = comb.icmp ceq %5, %16 : i3
^
results/alu.smt_generated_from_hw.mlir:31:11: note: see current operation: %28 = "comb.icmp"(%5, %27) <{predicate = 10 : i64}> : (i3, i3) -> i1
Could you send me an example of how to execute the commands?
Representing stateful circuits in SMTLIB is fundamentally non-trivial since SMTLIB has no concept of state/procedure/time (i.e., there's not really a clear way to represent a register in SMTLIB). Bounded model checkers tend to handle the issue by building a new set of constraints in the SMT problem for each cycle, and invoking the SMT/SAT solver on each cycle (or by combining all the unrolled states into one invocation).
There are some ways to encode things like reachability in SMTLIB though, using e.g. Constrained Horn Clauses, so you can check a bad state isn't reachable. Do you have a specific use-case in mind?
It seems that in yosys it works so that it creates a transition function in smt, and then unwinds it to a specific number of bmc cycles, if necessary. As far as I understand, it is legal to create transition functions in smtlib, and if this is indeed the case, then I don't see any fundamental limitations.
Ah yeah, I took a look at the Yosys flow and I think that emitting the transition functions as they do should definitely be possible. We don't have any proper infrastructure since this isn't a use-case we've come across before, but if you're interested in working on it I think it should totally be doable. As a start you may actually be able to get something pretty similar to a transition function by running the ExternalizeRegisters pass on your hardware design, which replaces registers with inputs/outputs to the circuit (effectively as if the register was moved out of the module, with its input and output flowing through the module barrier). If you run that before you pass anything through this flow, then the output assertions generated in the SMTLIB will correspond to the values of the outputs and registers based on the inputs and current state, so pretty much a transition function!
I think that's what I need, but I still can't get it to work.
➜ smt_check circt-opt --convert-comb-to-smt results/alu.hw.mlir results/alu.hw.mlir:14:10: error: failed to legalize operation 'comb.icmp' that was explicitly marked illegal %0 = comb.icmp ceq %op, %c0_i3 : i3 ^ results/alu.hw.mlir:14:10: note: see current operation: %22 = "comb.icmp"(<<UNKNOWN SSA VALUE>>, %21) <{predicate = 10 : i64}> : (i3, i3) -> i1 ➜ smt_check circt-opt --convert-comb-to-smt results/alu.smt_generated_from_hw.mlir results/alu.smt_generated_from_hw.mlir:31:11: error: failed to legalize operation 'comb.icmp' that was explicitly marked illegal %17 = [comb.icmp ceq](https://github.com/llvm/circt/blob/57e463bb5fe8ad133b5e197964835b26fd5249e4/lib/Conversion/CombToSMT/CombToSMT.cpp#L57) %5, %16 : i3 ^ results/alu.smt_generated_from_hw.mlir:31:11: note: see current operation: %28 = "comb.icmp"(%5, %27) <{predicate = 10 : i64}> : (i3, i3) -> i1Could you send me an example of how to execute the commands?
I'm guessing this IR has come through the Verilog front-end - I've seen that this front-end tends to produce ceq comparisons, which don't have an SMTLIB analogue. A temporary fix would be for you to just to find-and-replace all occurrences of comb.icmp ceq with comb.icmp eq, which should be a valid transformation under the assumption your inputs will always be two-valued. I wonder if the Verilog front-end produces ceq predicates in places where eq is definitely safe though - @fabianschuiki any idea if this is the case? I would assume that replacing the ceq with eq is fine as long as the case pattern contains no Xs or Zs?