Modularise the specification

Alasdair commented 1 month ago

I am opening the PR primarily to get feedback on one of the main things I have been slowly working on w.r.t. the sail-riscv model.

Right now the model is (in my opinion) a bit 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 using the Makefile does not allow for extensions to easily be added and removed without hand-modifying the Makefile.

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 you pass a list of files to Sail on the command line today), 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

I have included an updated Makefile in this PR, which you can invoke using make -f Makefile.new csim

The initial splitting of the model is something that I would like feedback on. I have tried to split it roughly so each extension is its own module, or grouped collection of related modules. There are some improvements I could make if I modified the model source slightly to move things around, but for this PR you'll notice I haven't changed the model source at all.

Feedback on the structure of the .sail_project file is also appreciated - do you think it needs additional features, is it understandable what it means at a glance?

Note there were some bugs I had to squash when putting this PR together, so it only builds with the development version of Sail - I expect this feature to be usable by the next release, taking into account any feedback I get here.

github-actions[bot] commented 1 month ago

Test Results

396 tests ±0 396 :white_check_mark: ±0 0s :stopwatch: ±0s 4 suites ±0 0 :zzz: ±0 1 files ±0 0 :x: ±0

Results for commit e1082d22. ± Comparison against base commit 47380fa5.

billmcspadden-riscv commented 1 month ago

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 https://github.com/riscv/sail-riscv/commit/e1082d22e03f3f956cce3d51e7c64574078915ae. ± Comparison against base commit 47380fa https://github.com/riscv/sail-riscv/commit/47380fa5c5025366423766ea3ffa37a7bfac780c .

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/pull/572#issuecomment-2391798531, 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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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.

Alasdair commented 1 month ago

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.

riscv / sail-riscv

Modularise the specification #572

Test Results