SMT target and SystemVerilog target?

[zhanghongce]

In the Makefile, I see there is the riscv.smt_model target, I was hoping it can generate models in SMT-LIB2 format (is that what it means to be?), but it seems that does not work for me.

The error message is:

sail: unknown option '-smt_serialize'.
Sail 0.17.1 (sail @ opam-v2.1.2)

Can anyone help explain how to fix this?
Meanwhile, I was wondering, how to generate the reference ISA model in System Verilog?

Thanks!

[zhanghongce]

It seems that -sv option is for System Verilog target. But I encounter another error:

Internal error: Unreachable code (at "src/sail_sv_backend/jib_sv.ml" line 207):
model/riscv_types.sail:408.21-42:
408 |     " with xlen=" ^ dec_str(sizeof(xlen)))
    |                     ^-------------------^
    | dec_str
    | 
    | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 197, characters 18-62
    | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 205, characters 34-61
    | Called from Jib_sv.Make.Smt.dec_str in file "src/sail_sv_backend/jib_sv.ml", line 207, characters 17-58
    | Called from Libsail__Smt_gen.Make.builtin.(fun) in file "src/lib/smt_gen.ml", line 1184, characters 21-56
    | Called from Libsail__Smt_gen.bind in file "src/lib/smt_gen.ml", line 113, characters 15-30
    | Called from Libsail__Smt_gen.fmap in file "src/lib/smt_gen.ml", line 117, characters 14-17
    | Called from Libsail__Smt_gen.bind in file "src/lib/smt_gen.ml", line 112, characters 14-17
    | Called from Libsail__Smt_gen.run in file "src/lib/smt_gen.ml", line 133, characters 14-17
    | Called from Jib_sv.Make.sv_checked_instr in file "src/sail_sv_backend/jib_sv.ml" (inlined), line 762, characters 15-49
    | Called from Jib_sv.Make.sv_fundef in file "src/sail_sv_backend/jib_sv.ml", line 792, characters 33-55
    | Called from PPrint.separate_map.(fun) in file "src/PPrint.ml", line 131, characters 21-24
    | 
    | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues