Add sail_project file to modularise the specification

[Alasdair]

Use the Sail module system to organise the files in the model. Rather than passing a list of files on the command line, the files are specified using the model/riscv.sail_project file.

The previous version uses a big flat list of files which is unwieldy and hard to understand as it is not clear immediately what the high level structure of the model is, and the way we configure the model does not allow for extensions to easily be added and removed without hand-modifying the CMake. This doesn't matter for the C backend but it does for formal/SV backends.

To solve this problem, I have added a basic module system to Sail, which allows for the structure of the specification to be specified as a collection of modules in a .sail_project file. The key ideas here are as follows:

• Each of these modules consists of a list of files (much like how we passed a list of files to Sail on the command line previously), as well as a list of modules that module requires.

• The module system ensures that if a module does not require another module, it cannot refer to any definitions contained within it. There is also a private keyword which can be used to encapsulate implementation details.

• Modules can specify other modules that must come before or after them, but without requiring them. This is to support the scattered definition feature.

• The .sail_project file serves as an instant reference to the overall model structure, it isn't embedded in the files. You can also have multiple .sail_project files, so you could pass riscv.sail_project cheri.sail_project to Sail, and it would be able to link them together in much the same way we do now.

• There is some basic support for conditional includes.

With this, building the model becomes as simple as:

sail --project model/riscv.sail_project --variable ARCH=RV64 --all-modules

[github-actions]

Test Results

2 099 tests  ±0   2 099 ✅ ±0   17m 52s ⏱️ -12s
    1 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit 814d29b. ± Comparison against base commit 0fb44db.

♻️ This comment has been updated with latest results.

[billmcspadden-riscv]

First of all, I think this is a good idea and needs to be pursued. However, as the model stands now, it would seem to be a bit difficult to split up files based on extensions. I'm specifically referring to the CSRs. They seem to be lumped together and not tied to an extension. For example, the HPM CSRs are listed in the riscv_csr_begin.sail file. It seems like they should be put into an "hpm extension" file. Also, the implementation of some individual CSRs is based on multiple extensions. The simplest one I can think of is the misa CSR. As an example, how would a vector module implement the V bit in the misa? How can that functionality be scattered? Bill Mc.

…

On Thu, Oct 3, 2024 at 9:07 AM github-actions[bot] ***@***.***> wrote: Test Results 396 tests ±0 396 ✅ ±0 0s ⏱️ ±0s   4 suites ±0   0 💤 ±0   1 files ±0   0 ❌ ±0 Results for commit e1082d2 <e1082d2>. ± Comparison against base commit 47380fa <47380fa> . — Reply to this email directly, view it on GitHub <#572 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXROLOFN5YVVISH37OTGVM3ZZVTUXAVCNFSM6AAAAABPKC4BVGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGOJRG44TQNJTGE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

-- Bill McSpadden Formal Verification Engineer RISC-V International mobile: 503-807-9309 Join me at RISC-V Summit North America <http://www.riscvsummit.com/> in October!

[Alasdair]

Everything in the riscv_csr_begin file should be fairly easy to split up, especially with some of the work Tim has done recently cleaning that up.

When it comes to things like bits in the misa register, I think it might just not matter too much - bit 21 of the misa register exists whether or not you have the V extensions, so giving it a name in a common file isn't necessarily a big deal. I did experiment with something like:

bitfield Misa : xlenbits = {
  $[in_module V_ext] V : 21
}

(using an attribute just to avoid any concrete syntax for now) where you could push the definition of a field into another module without making it a scattered definition, but I'm not sure it's really needed.

[Alasdair]

I have also considered adding a feature that would allow you to require a module in such a way that you can only use it in a guarded way, i.e. from the riscv_core module you could do something like guarded_require Foo_ext, then you would have to use an if-statement or similar whenever you access the module:

if extension_exists(Foo_ext) then {
  some_foo_ext_function() // would raise an error if used outside the if
}

The way that would work is it just combines Sail's existing flow-sensitive typing with the 'in_scope' check the type-system now does, and it means you can add functionality to the base model from an extension in a way where we can statically guarantee it gets compiled out when the extension doesn't exist.

[Timmmm]

This looks like a huge improvement. I think even if it doesn't solve all the modularisation & organisation issues we should switch to it ASAP.

Does the private keyword mean that no other modules can refer to that definition even if they say they depend on it? That sounds very useful too.

I think when this is done we should work on improving the organisation of the modules and maybe reducing their size. There are a few places in the code where people have just kind of given up, e.g. this one:

 * NOTE: This would be better placed in riscv_platform.sail, but that file
 *       appears _after_ this one in the compile order meaning the valspec
 *       for this function is unavailable when it's first encountered in
 *       read_seed_csr. Hence it appears here.
 */
val get_16_random_bits = impure {
    interpreter: "Platform.get_16_random_bits",
    c: "plat_get_16_random_bits",
    lem: "plat_get_16_random_bits"
} : unit -> bits(16)

[Alasdair]

Does the private keyword mean that no other modules can refer to that definition even if they say they depend on it? That sounds very useful too.

Exactly, if you have amod.sail with:

private function foo(message : string) -> unit = {
  print_endline(message)
}

and another file bmod.sail with:

function main() = {
    foo("Cannot be called")
}

and link them like:

A {
  files amod.sail
}

B {
  requires A
  files bmod.sail
}

You'll get an error like

Type error:
bmod.sail:5.4-7:
5 |    foo("Cannot be called")
  |    ^-^
  | Cannot use private definition
  | 
  | amod.sail:3.17-20:
  | 3 |private function foo(message : string) -> unit = {
  |   |                 ^-^ private definition here in A

I think there are a few places in the virtual memory code where we have something like // Private as a comment, so I wanted to make sure that could be made an actual thing.

[jordancarlin]

Seems like a great improvement.

It might be worth thinking about how we nest the extensions though.
For example, is B supposed to represent the B extension (seems most intuitive) or just all bit-manipulation extensions in general? Currently Zbc is nested under B despite not being part of the B extension. A similar discrepancy exists for Zcb being part of C.

[Timmmm]

What's the significance of the nested modules? Is it that riscv_insts_zba.sail can't use anything from riscv_insts_zbb.sail?

Another question: is the intention that you can exclude modules from compilation? I mean I don't think we would want that for the C simulator use case (except maybe to exclude Vector for compilation time reasons), but I guess you might want that for the SV backend?

// RISC-V Bit manipulation extensions
  B {
    requires riscv_core, riscv

    Zba {
      files riscv_insts_zba.sail
    }
    Zbb {
      files riscv_insts_zbb.sail
    }
    Zbc {
      files riscv_insts_zbc.sail
    }
    Zbs {
      files riscv_insts_zbs.sail
    }
  }

[Alasdair]

Currently the module namespace is flat, and the nesting just allows you to require a group of related modules, so the following

A {}

B {
  requires A
  C {}
  D {}
}

E {
  requires B
}

is equivalent to

A {}
B { requires A }
C { requires A, B }
D { requires A, B }
E { requires B, C, D }

so requires M means require M and any child modules of M. Modules implicitly require their parents, and inherit any requires from them.

[Alasdair]

Another question: is the intention that you can exclude modules from compilation?

Yes, rather than giving Sail a list of files you can give it a list of module names and it just uses them. The --all-modules flag is what makes it just include everything.

[Timmmm]

Did you have any idea how this would work with the CHERI repo? I guess the simplest thing is to just copy & paste the whole file and then change all the riscv_s to cheri_s where appropriate.

Or maybe add a load of if $CHERI then..? Hmm.

[Alasdair]

The idea was you could have riscv.sail_project and cheri.sail_project and pass both to Sail. However that likely only works if the second set of modules is strictly additive or only provides implementations for the kind of pre-placed hook functions ext_something that we have right now. The worst case is you would just copy it and modify it, but in practice that isn't different to the way it's currently set up with a git submodule and a separate makefile, so the worst case here isn't really all that bad.

[jordancarlin]

This would be a good PR to revive so that we can get some of the last RVA23 extensions (hints and control flow) that are waiting on it into the model. Especially now that initial configuration support is merged. @Alasdair I assume that now that Sail 0.19 is released all of the necessary features for this should be available?

[Alasdair]

Just need to update this to CMake and make sure any new files since this was added are included

[Alasdair]

Rebased, and update to use CMake. Let's see what the CI thinks...

[Alasdair]

Down to a single error in the Lean output about undefined_HpmEvent. Not sure what's causing it.

[pmundkur]

Some dependencies don't seem to be required.

[Timmmm]

I rebased this, added the unit tests Sail code and addressed the review comments. Hope that's ok! I think we should merge this now.

[Alasdair]

I now have a minimal example to reproduce the Lean issue, so hopefully I will have it fixed upstream in Sail soon.

[Timmmm]

I think the Lean is broken due to #1086 now too, so I think we should merge this now anyway.

Also I noticed that we now do the classic for-case antipattern, so the CMake can be simplified a fair bit. I have a commit ready to do that after this is merged.

[Alasdair]

I have fixed the Sail to Lean bug now, so CI should start working when I get it merged.