F# RISC-V Instruction Set formal specification

by mrLSD-dev • 3 years ago

134 42 3 years ago

mrLSD-dev9• 3 years ago

RISC-V CPU formal specification written on F#. Formalazation of RISC-V ISA architecture.

thumbuddy2• 3 years ago

I know F#, I know roughly what RISC-V is. Not sure I understand the high level though. Is it that they formalized the instructions set in F# or is it that F# now can use the formal instruction set to compile programs?

Sorry this isn't my wheelhouse but I am curious.

mrLSD-dev9• 3 years ago

Due to the properties of F# as a functional language, using a pure representation of functions and a strong type system - in this case, this is a formalization of RISC-V ISA (instruction set). Since we don't have side effects for pure functions. As it has a State machine, one fun opportunity is to execute elf-bin files for it for RISC-V architecture.

I'm not sure what do you mean "compile programs", because it's not the compiler.

kevingadd2• 3 years ago

Always fun to see executable specs. For a bit I was experimenting with using F# to write the WebAssembly specification. We ended up using OCaml.

foderking• 3 years ago

why ocaml instead

kevingadd2• 3 years ago

I don't think it was a formal decision that got made at any point, so there wasn't any particular reason. When someone else started writing the actual spec he picked Ocaml. It ended up probably being the wrong choice in the short term (we had to reimplement 32-bit floats in software, and for a while we couldn't run the ocaml files on windows very easily) but in the long term it seems like it worked out OK.

I kind of wish we had used a theorem prover language of some sort though since we had the opportunity to do so. I didn't really have the chance to change things there since other people had higher seniority than me.

brucehoult• 3 years ago

I remember in 1982 or 1983 we had a very very slow implementation of Ada on our university VAX that was written at NYU as an executable specification in a language called SETL.

wheresmycraisin• 3 years ago

Can anyone ELI5 this? Is it basically an emulator?

IshKebab2• 3 years ago

Basically yes, but with the goal being semantic correctness rather than performance.

Seems to be similar to the official Sail model but F# instead of Sail.

Kind of funny since Sail can already compile to OCaml - probably wouldn't be too hard to add a F# backend. Then again, more independent implementations are always nice to have.

Would be interesting to know their motivation for this.

Edit: actually this looks like it has been dead for 3 years so maybe it was just a precursor to the Sail model.

https://github.com/riscv/sail-riscv

mrLSD-dev9• 3 years ago

It's possible to emulate. But not only. The main goal is to formalize the representations of the RISC-V instruction set (ISA), decoder, executor, and state machine. So it's more formal point of view for RISC-V ISA.

jsomedon• 3 years ago

the RISC-V instruction set (ISA), decoder, executor, and state machine

So does this repo define these things as F# function and as a user I can import this repo as library and call those functions and my function call would directly run instructions on RISC-V processors, with no "middlewares" like operating system and such?

mjfl• 3 years ago

Very cool. Does this allow simulation / verification of L1/L2 cache usage?

mrLSD-dev9• 3 years ago

unfortunately not, because it does not apply directly to ISA. However, the idea is interesting.

ArtixFox3• 3 years ago

thats cool! Is there any project that does this for other architectures?

kristiandupont• 3 years ago

I created this for x86 many years ago: [link redacted]

It's not an emulator, it allows you to assemble code in C++ at runtime. It breaks down the architecture (as it looked at the time) quite detailed, if you are interested :-)

EDIT to add: the .cbi file is a text file that contains most of the documentation: [link redacted]

ArtixFox3• 3 years ago

thank you!!

JonChesterfield2• 3 years ago

Right there with you. I'd love one of these for x86-64 or amdgpu. Assemblers are good things (like the sibling to this) but it's a huge effort to translate the ISA docs to an executable representation.

If you've got that encoding <-> code mapping though, you can turn that into an assembler, an emulator and a compiler backend with a sufficiently determined code generator. Probably a profiler and debugger too. That's a whole set of tooling derived from a single source of truth. In the best case, you persuade the people writing the verilog to provide said information as something like xml. More likely it's an error prone transcription from incomplete pdf files.

ArtixFox3• 3 years ago

aw hell yeah, something like this could be ridiculously useful. Been playing with my own interactive low level language[glorified forth, dont wanna touch C and friends again.] and something like this would make life super easy.

davidgrenier3• 3 years ago

I think this qualifies?

https://en.wikipedia.org/wiki/MMIX#Simulators_and_assembler

IshKebab2• 3 years ago

There are Sail models for ARM, RISC-V, x86 and MIPS. I think ARM has its own executable spec too.

nullifidian5• 3 years ago

Is this subset of F# itself formally specified? How is it different from an emulator that is slightly more clear to read?

davidgrenier3• 3 years ago

My understanding of this is that it is an emulator that is meant to be very clear to read.

davidgrenier3• 3 years ago

It isn't though: https://github.com/mrLSD/riscv-fs/blob/fa039b123ded9fa0c05d0...

mrLSD-dev9• 3 years ago

Since F# is a functional language, it allows, using a purely functional approach and a system of strong types, pure functions, to formally verify the correctness of a particular ISA. The emulator is nothing more than a side effect.

nullifidian5• 3 years ago

it allows to formally verify the correctness of a particular ISA

That must be hypothetical. "Functionalness" of the language/code doesn't make everything that is written automatically subject to formal verification. (mechanized or pen and paper). What kind of correctness properties does it actually allow to formally verify? I understand if it was the F* language, which is a full blown dependently typed proof checker, but with F#, which is defined by the implementation and 300 page English spec, I don't think you can verify anything interesting. As far as I know F# itself doesn't have mechanized formal semantics and its type system could be unsound.

https://github.com/mit-plv/riscv-coq and https://github.com/riscv/sail-riscv (don't know how complete they are) approaches actually allow to formally (mechanically) verify riscv properties.

Your executable specification could probably be called "Formal", in the same sense as a PDF spec being called "Formal", but being subject to verification by the virtue of F# being functional or being written in the functional style might be pushing it too far.

FrustratedMonky• 3 years ago

Just glad to see F# used for something and hitting front page.

Such a great language, it never seems to get traction, to hit any critical mass.

mrLSD-dev9• 3 years ago

The main competitor of Haskell, and also not the most popular language. However, the only way to popularize a language is to write in it. This project is trying to reveal the possibility of F#, and show the worthy side of F#,

F# RISC-V Instruction Set formal specification

Related Stories