Add info about supported ISA extensions to README

[Columbus240]

The information was taken from the type InstructionSet, defined in src/Spec/Decode.v.

Documenting the capabilities of the current model seems useful to me. So people foreign to the project can know what to expect. The specific wording and formatting is not important to me, change it as you like. (If you accept the PR)

[Columbus240]

I didn’t want the second commit to turn up in this pull request and don’t know GitHub well enough to remove it.

[samuelgruetter]

Thanks, I just cherry-picked the first commit onto master.

[Columbus240]

While reading a little more of the codebase I found out that only I and M instructions have an execution function implemented, and that CSR related instructions aren’t supported yet. (src/Spec/Execute.v) Decoding of A and F instructions seems to be fully implemented. (src/Spec/Decode.v) So my patch was wrong. Could you please change the README.md accordingly?

riscv-semantics has implemented both A and F. A is relatively simple, because there is only one hart, the instructions are implemented like the I instructions. The F instructions need new registers in the RiscvMachine and an implementation of floating-point numbers.

The A extension looks simple enough to me, that I’ll try implementing it myself.

[samuelgruetter]

Are you aware of the convert target in the Makefile? It's used to automatically generate Decode.v and Execute*.v files from Haskell, so don't write these Coq files manually.

[Columbus240]

Thank you for pointing convert out. I thought there must be something like it, but didn’t look for it. Right now I couldn’t get it to work, maybe some other time. I wrote ExecuteA.v by hand now, and found that the code is so abstract, that Coq gives incomprehensible error messages about the type inference when I make errors and the typing problem becomes unsolvable. :D

I noticed that the instructions LR_w and SC_w of the A extension need additional state in RiscvMachine to implement the reservation mechanism. The spec allows many different implementations of the reservation mechanism. I thought of the following solution in Coq: Abstract over the implementation of the reservation mechanism using a Class or similar, forcing it to conform to the requirements of the spec. Then add a member of this Class to the RiscvMachine and implement the execution behaviour as needed. Finally, provide a minimal instance of the Class that can be used in Example.v and in similar places.

The Haskell code has an abstraction over the memory (Spec/Memory.hs), that isn’t used in the definition of the RiscvMachine typeclass, but in the instances of it (see Platform/Minimal*.hs and Utility/MapMemory.hs). Encapsulating the properties of the memory in its own typeclass might be useful for the Coq.

The Monad type in Utility/Monads.v seems to have the (syntactic) structure I’m imagining (functions followed by axioms the functions have to adhere to). I’ll submit a PR or an issue when I think I have something.

[samuelgruetter]

Coq gives incomprehensible error messages about the type inference when I make errors and the typing problem becomes unsolvable. :D

I know exactly what you're talking about, these error messages are quite painful :wink:

If you want to have the A extension in Coq, I'd recommend following what's done in Haskell as closely as possible, because eventually we might want to automatically translate more files than just Decode.v and Execute*.v.

[Columbus240]

The automatic translation is currently problematic in a few cases. As it is now, the Haskell allows RiscvMachines, whose store* and load* are unrelated and/or don’t do anything. Constraints that could be expressed in Coq using dependent types. During or after translation the missing constraints would need to get added. For example by wrapping the translated types with typeclasses or records containing the constraints.

I understand that you don’t want to keep the two repos in sync by hand.

[Columbus240]

Of course, I’ll try to copy the structure and the formatting of the existing code when I do changes.