[SMT] How to go from Verilog to smtlib2 like with Yosys?

[flaviens]

Hi there!

I was exploring whether it was possible to export some simple design from verilog to some smtlib2 representation like with Yosys.

The following naive experiment produced an empty file.

my_or.v

module my_or (
    input  logic a_i,
    input  logic b_i,
    output logic y_o
);
    assign y_o = a_i | b_i;
endmodule

The commands I run:

circt-verilog my_or.sv -o my_or.mlir
circt-opt --convert-hw-to-smt --convert-comb-to-smt my_or.mlir -o my_or_postop.mlir
circt-translate --export-smtlib my_or_postop.mlir -o my_or.smt2

Do you have some indications?
Thanks!
Flavien

[dobios]

Maybe @TaoBi22 @maerhart would know?

[dobios]

Hey Flavien!
It's really cool to see that you are trying to use CIRCT more!!

Can you show what you're getting in your my_or.mlir?

Note: CIRCT has it's own bmc tool if that can help, alternatively you can also hook up to external bmc tools using the btor2 target (firtool --btor2 my_or.mlir >> my_or.btor2)

[TaoBi22]

Hey @flaviens! Yeah, I think I know what the problem is here but @maerhart might be able to confirm. Currently the SMTLIB infrastructure we have is just focused on our internal verification tooling, so the SMT dialect operations correspond to building nodes of the SMTLIB AST, rather than actually building standalone operations. This means that although your SMT dialect file in or.mlir contains the construction of all the nodes in the AST, there's no assert command to actually build an assertion with the AST to put in the SMTLIB file. This is better for our verification tools as it trims away unnecessary cruft that has nothing to do with the assertion, but not very useful for this purpose.

We should definitely document this better, sorry for the confusion! A workaround for now might just be to add a verif.assert operation to the end of or.mlir - at some point we probably want to add a flag to the SMTLIB export that lowers each operation to a value definition (i.e. %0 = comb.and %1, %2 directly becomes (assert (eq (val0) (and val1 val2))) but I don't think we support that right now.

[maerhart]

Hi Flavien, thanks for checking out the SMT lowering!
@TaoBi22's analysis is correct. We currently don't emit any SMT ops that don't have any uses.
Additionally, the HWToSMT pass is currently a bit biased towards the SMTToLLVM lowering because it emits functions (func.func) for hw.module operations (which is what you get from your SV module). We are essentially missing a small transformation that takes the top-level module and inlines its body into a smt.solver operation. The SMTLIB export pass iterates over these solver operations for emission. In your example, there is no such solver op so everything is just ignored (regardless if there are asserts in there or not).

I agree that we should add such a pass (or modify HWToSMT) and also support emitting SMT ops that are not in a solver scope.

[flaviens]

Hi there,

Thank you for all the answers!

Here are the file contents:

• my_or.mlir

module {
  hw.module @my_or(in %a_i : i1, in %b_i : i1, out y_o : i1) {
    %0 = comb.or %a_i, %b_i : i1
    hw.output %0 : i1
  }
}

• my_or_postop.mlir

module {
  func.func @my_or(%arg0: !smt.bv<1>, %arg1: !smt.bv<1>) -> !smt.bv<1> {
    %0 = smt.bv.or %arg0, %arg1 : !smt.bv<1>
    %1 = builtin.unrealized_conversion_cast %0 : !smt.bv<1> to i1
    %2 = builtin.unrealized_conversion_cast %1 : i1 to !smt.bv<1>
    return %2 : !smt.bv<1>
  }
}

I tried adding assertions in the sv file but I couldn't write any that is accepted by the circt frontend (I might have done something wrong). I also tried adding verif.assert in the mlir file but circt was unhappy, I have in fact no experience in where to put it exactly and which operands to provide, so I cannot say yet whether it is a suitable workaround.

Do you have concrete ideas how to work around the current state to produce some smt2 output?

Thanks!
Flavien