search

mit-plv / riscv-semantics

A formal semantics of the RISC-V ISA in Haskell
BSD 3-Clause "New" or "Revised" License
156 stars 16 forks source link

Why Formal #34

Open ThePerfectComputer opened 1 year ago

ThePerfectComputer commented 1 year ago

What makes this codebase a formal model? I ask because I'm currently writing a model for a CPU I'm designing in Haskell, and I want to know what a model has to have to be called "formal".

samuelgruetter commented 1 year ago

It's formal in the sense that it enables its users to apply formal methods, ie to reason with mathematical proofs about the behavior of their hardware and/or software. You can read more about how we did that in this preprint paper.

ThePerfectComputer commented 1 year ago

Oh wow! That paper is really cool. Incidentally, I have been using Clash for some other projects.

ThePerfectComputer commented 1 year ago

Lines like these seem a bit verbose and redundant... https://github.com/mit-plv/riscv-semantics/blob/master/src/Spec/Decode.hs#L17-L21

I could conceive of perhaps:

data LoadType = LoadType  { rd :: Register, rs1 :: Register, oimm12 :: MachineInt }

data InstructionI =
  Lb LoadType |
  Lh LoadType |
  Lw LoadType |
  Lbu LoadType |
  Lb LoadType |
  Lhu LoadType

Why such a verbose approach?

ThePerfectComputer commented 1 year ago

Also - perhaps this isn't the appropriate place for this conversation. I'm genuinely intrigued by this codebase at a basic level - and I suppose I have a number of questions...