6 ms·
F# RISC-V Instruction Set formal specification
- mrLSD-dev 3y agoRISC-V CPU formal specification written on F#. Formalazation of RISC-V ISA architecture.
- thumbuddy 3y agoI 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-dev 3y agoDue 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.
- thumbuddy 3y agoI think the right word would have been 'execute' programs. Not compile. Thanks for explaining.
- kevingadd 3y agoAlways 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 3y agowhy ocaml instead
- kevingadd 3y agoI 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.
- JonChesterfield 3y agoI'm slowly coming around to SML and HOL as the best available tools for stuff like the op. In particular cakeml and candle look suspiciously like a solid foundation for modelling instruction sets.
- brucehoult 3y agoI 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 3y agoCan anyone ELI5 this? Is it basically an emulator?
- IshKebab 3y agoBasically 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 https://github.com/riscv/sail-riscv
- mrLSD-dev 3y agoIt'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 3y 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?
- mrLSD-dev 3y agoYou can easily import and use specific functions for the decoder, or executor for specific ISA. Or even use the whole state machine. And this is represented by tests. Those. any single RISC-V architecture instruction, or an entire program. Because it can be used as a cpu emulator. Those. OS doesn't matter in this case. However, I draw your attention to the fact that this is only a processor, and not an emulation of the PC and its peripherals.
- mjfl 3y agoVery cool. Does this allow simulation / verification of L1/L2 cache usage?
- mrLSD-dev 3y agounfortunately not, because it does not apply directly to ISA. However, the idea is interesting.
- ArtixFox 3y agothats cool! Is there any project that does this for other architectures?
- kristiandupont 3y agoI 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]
- ArtixFox 3y agothank you!!
- JonChesterfield 3y agoRight 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.
- ArtixFox 3y agoaw 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.
- davidgrenier 3y agoI think this qualifies? https://en.wikipedia.org/wiki/MMIX#Simulators_and_assembler https://en.wikipedia.org/wiki/MMIX#Simulators_and_assembler
- nullifidian 3y agoIs this subset of F# itself formally specified? How is it different from an emulator that is slightly more clear to read?
- davidgrenier 3y agoMy understanding of this is that it is an emulator that is meant to be very clear to read.
- davidgrenier 3y agoIt isn't though: https://github.com/mrLSD/riscv-fs/blob/fa039b123ded9fa0c05d00e4854e4c721e8ec0dd/CLI.fs#L77 https://github.com/mrLSD/riscv-fs/blob/fa039b123ded9fa0c05d0...
- genter 3y agoAs far as F#/OCaml goes, that's excellent. (I'm convinced one of the reasons why Rust is so popular is because it's OCaml with a legible syntax.)
- pharmakom 3y agoF# has diverged quite a lot from OCaml and is very readable IMO. In any case, I think this view stems from our Algol/c/Java centric CS education system that casts ML and Lisp as weird and “unreadable”, when really it’s just a matter of perspective.
- jcelerier 3y ago> when really it’s just a matter of perspective. it's really not, in the engineering school I did in the first year we were taught both C and LISP during the same semester and it was obvious to almost everyone except math nerds how much easier C was mapped to a normal human being (e.g. someone without prior programming experience)'s mental model of the world
- 3y ago
- FrustratedMonky 3y agoJust 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-dev 3y agoThe 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#,
- deleted 3y ago[deleted]