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

[westtide]

To generate models in SMT-LIB2 format using Sail, you'll need to enable detailed SMT output by modifying the source code. Here’s how to do it step-by-step:

1. Clone the Sail project from GitHub: git clone https://github.com/rems-project/sail.git
2. Go to the src/lib/constraint.mlfile and change the line: let opt_smt_verbose = ref false to let opt_smt_verbose = ref true. This will set the optional Boolean value to true, allowing detailed SMT information to be printed.
3. Install OPAM and build the Sail project from source code. Follow the instructions here.
4. Switch to the Sail-RISCV project. In the Makefile, update the riscv.smt_model target to ensure compatibility with Sail version 0.18. The flag should be changed to -smt.
5. Run the following command to generate the SMT model: make riscv.smt_model

[Alasdair]

Was that answer generated (i.e. hallucinated?) by a LLM? Because it's completely wrong.

Currently the Sail->SMT backend generated SMT files for boolean functions marked with either the $property (for things expected to be true) or $counterexample (when expected to not hold) attributes. You can use this to prove properties of simple functions, essentially like unit tests but verified for all inputs.

[Alasdair]

I think that Makefile target is out-of-date now, afaik it was for a experimental memory-model tool we had that subsequently got replaced by https://github.com/rems-project/Isla. The problem was generating a SMT definition for the entire behaviour of the ISA was far too slow and difficult for the SMT solver to handle, so we switched to a symbolic execution approach that therefore only generates SMT for the paths it needs to execute for a given test.

[westtide]

Hi there, thank you for your response, and apologies for my tone.

Initially, I was trying to find something related to SMT-LIB in the -help options and encountered the same issues as described in this thread. After reviewing the Sail parameters, I noticed that some arguments in the sail-riscv Makefile were incompatible. Therefore, I turned to the source code to look into related functions, such as set_solver, call_smt, and solve_smt_file in constraint.ml, and found opt_smt_verbose.

I have read related papers about Isla, and it seems like a good solution for my needs. I'll take a closer look at the implementation. Thanks again.