D extension (double precision float) support should be a runtime option

[Timmmm]

Currently to choose between F support or F&D you need to compile the model differently - using riscv_flen_D.sail or riscv_flen_F.sail.

This is unfortunate because now to support all the different configurations you need to compile a combinatorial explosion of models:

• rv32_F
• rv32_D
• rv64_F
• rv64_D

(and 4 more if you want CHERI models)

It would be better if it was a runtime option (though this may lead to slightly less neat and type-safe code unfortunately).

---

@Alasdair I wonder if Sail could help here by supporting values that are compile-time constant for Sail, but runtime configurable in the generated code. I.e. instead of this:

type flen       : Int = 64
type flenbits         = bits(flen)

you'd have

type flen       : Int = oneof(32, 64)
type flenbits         = bits(flen)

and then it would compile it as if flen could be either 32 or 64 (but it must be constant). Then in the generated C/OCaml code you would be able to set it at runtime (maybe as a parameter to model_init()). This would also help for RV32/RV64.

I guess this is a large amount of work... I'm just thinking aloud. :-)

[Alasdair]

I have toyed with allowing

// Abstract type, with no value
type flen : Int

// Global constraint
constraint flen in {32, 64}

You could even do something like

type flen : Int
type have_D_ext : Bool

constraint flen in {32, 64} & implies(have_D_ext, flen == 64) 

[Timmmm]

constraint flen in {32, 64}

How hard would this be to implement? Just wondering if I might have a go to save compiling separate RV32 and RV64 models.

[Alasdair]

A bit tricky as it has an effect throughout the entire compiler.

I had an implementation that went as far as the parser and type system aspects, let me see if I can drag those commits to the present.

[Alasdair]

There are also a few implementation questions, like whether to allow things like

type abstract('n: Int) : Int

because that makes sense for the type system, but we would need to instantiate that before generating C.

[Alasdair]

https://github.com/rems-project/sail/tree/abstract_types will build with a lot of warnings and probably fail if you use anything other than --just-check for the time being.