Change XLEN and FLEN to be configure-time options

[Timmmm]

This means you only need to compile the emulator once in order to support RV32F, RV32D, RV64F and RV64D. The emulator binary has been renamed to sail_riscv_sim.

XLEN is controlled by the base.xlen config value. FLEN is controlled by extensions.{F,D}.supported.

Some backends (Lean etc.) still need a compile-time config so for those we still support building multiple configs.

[pmundkur]

This is awesome! It looks like the upstream issues are fixed. Are there any other issues preventing this coming out of draft?

[Timmmm]

This is awesome! It looks like the upstream issues are fixed. Are there any other issues preventing this coming out of draft?

Getting closer but I hit another issue: rems-project/sail#1251

[Timmmm]

Also I need to:

1. Re-enable/fix the tests.
2. Remove flen or F/D as @jordancarlin suggested.
3. Maybe make the config option be xlen instead of log2_xlen_bytes which is not very intutive! Since there are only 2 options I think we can just go backwards like: type xlen_bytes : Int = if xlen == 32 then 4 else 8. Hopefully that will work.
4. Update the readme.
5. Ideally benchmark the performance hit. I suspect it will be relatively minor but it might not be.

And we'll need to wait for a new Sail compiler release after it's working.

[Timmmm]

Ok I got the RV64 first party test passing! Still need to do all the todos I mentioned.

[Timmmm]

I did have a crazy idea - what if we just take the xlen setting from the ELF file? :-D

On balance, probably a bad idea. Explicitness is good. Just thought I'd mention it!

[jordancarlin]

I did have a crazy idea - what if we just take the xlen setting from the ELF file? :-D

On balance, probably a bad idea. Explicitness is good. Just thought I'd mention it!

Something to think about down the road maybe. I think we can technically even find out which extensions an elf was compiled with if we really wanted to. Might be nice to be able to just run an elf without thinking about the config.

For verification purposes though (which I think is one of the primary uses of the Sail model), you want the model to exactly match an implementation no matter what the elf file being passed in is. Maybe there could be two different modes in the future: use the values from a config file if one is given and parse the elf if not.

[Timmmm]

This basically works now. All the tests pass. Remaining todos:

1. Benchmark.
2. Come up with a better system for the config files than copy/pasting them. Though tbh if we only have 2/3 files that's maybe the best way anyway.
3. Ideally get rid of the weird _rv suffix on riscv_sim_rv, but I think that might be best deferred until we merge the RVFI version so there's only a single emulator.
4. Wait for new Sail compiler release.

[Timmmm]

This also needs changes to the types of the callback interface now (fbits -> sbits). I'll do it at some point.

[jordancarlin]

@Timmmm I updated the types for the callbacks to get this building again and then removed ${arch} from the c simulator. As discussed during the meeting, I've renamed the simulator sail_riscv_sim.

I also realized that we need to maintain separate targets for the theorem provers since they take a compile time config file, so I added those back in.

[jordancarlin]

Not sure why the SMT target is failing to populate the config values from the config file, but other than that, this seems to be working now (barring the new Sail release).

[Timmmm]

Thanks! LGTM - just a few minor nits.

[jordancarlin]

Other than waiting on the new sail release, I still need to sort out why all of the theorem provers (including the SMT target) are giving the following error:

Error:
riscv_vmem_utils.sail:47.63-106:
47 |function sys_misaligned_allowed_within_exp() -> range(0, 11) = config memory.misaligned.allowed_within_exp
   |                                                               ^-----------------------------------------^
   | SMT solver returned unexpected status 1

@Alasdair @Timmmm any ideas?

[github-actions]

Test Results

400 tests  ±0   400 ✅ ±0   1m 28s ⏱️ +3s
  1 suites ±0     0 💤 ±0 
  1 files   ±0     0 ❌ ±0 

Results for commit 7b8122f. ± Comparison against base commit f4a94a3.

♻️ This comment has been updated with latest results.

[arichardson]

I might be being dumb but this is giving the following error when building the SMT target:

Error:
riscv_device_tree.sail:190.25-56:
190 |  let clock_freq : int = config platform.clock_frequency;
    |                         ^-----------------------------^
    | Runtime configuration is not supported when generating code for target 'smt'
    | An explicit configuration should be provided with the --config option.

Reasonable, except it does use the --config option:

cd /home/me/workspace/sail-riscv/model && /home/me/workspace/sail-riscv/build/sail/bin/sail --smt -o /home/me/workspace/sail-riscv/build/model/model --require-version 0.19.1 --config /home/me/workspace/sail-riscv/config/rv32d.json prelude.sail ... lots of sail files ... main.sail

It happens when one of the config options is missing from the json file. Looks like part of one of my patches was also lost during the rebase. Pushed an updated version that should resolve these issues.

Come up with a better system for the config files than copy/pasting them. Maybe. Tbh I'm ok with copy/paste to start with.

Not sure that there is a better option than copy/pasting because there are various extensions that should be different between RV32/RV64. For example, Zcf should be on in RV32 but not RV64. Similar for the Sv* extensions.

These should be quite easy to handle with a simple CMake substition:

"Zcf" : { supported: @CONFIG_IS_RV32@ }
"Sv32" : { supported: @CONFIG_IS_RV32@ } (or True if it works for RV64).
"Sv48" : { supported: @CONFIG_IS_RV64@ }
and then just call configure_file() with those variables set appropriately.

[Timmmm]

I'm still slightly partial to just copy & pasting. It's only two files and I think it's unlikely to grow... and I think there's a lot of value in having the file in the source tree that people can easily copy & paste and modify without having to dig it out from the build directory.

Would you be ok with merging this as-is and using configure_file() later if it becomes a problem (e.g. if they get out of sync)?

[Timmmm]

I do think we could delete default.json and just use the rv64d one as the default though. There's no need for three files...

[arichardson]

I do think we could delete default.json and just use the rv64d one as the default though. There's no need for three files...

Yes if there are only two files I'd be happy with this.

[Timmmm]

Ok I think this is ready to go. I finally got around to benchmarking it. First 3 million instructions of booting Linux (this is not very many - it actually doesn't get through OpenSBI). With a recent sail2 commit:

• master: 53 kIPS
• This PR: 48 kIPS

Considering with the 0.19.1 compiler it's like 9 kIPS and nobody noticed, I think that's fine. It would be nice to work back up to ~500 kIPS which is what Sail was capable of a while ago, but we'll have to do some work for that. I have some ideas.

[pmundkur]

This is awesome! We should merge this soon to avoid more painful rebasing.

[arichardson]

This is great!

[jordancarlin]

Rebased again. Would definitely be nice to get merged soon since just about any change to the CMake or config files forces this be rebased.

[Timmmm]

Didn't notice your rebase so I also rebased, and we both made slightly different rebase mistakes which I have fixed. :-D

I will merge this today if nobody objects!