[libre-riscv-dev] spr formal proof, NLNet RFPs
Luke Kenneth Casson Leighton
lkcl at lkcl.net
Fri Jul 17 21:40:08 BST 2020
On Friday, July 17, 2020, Samuel Falvo II <sam.falvo at gmail.com> wrote:
> Registered as a personal account for the time being.
> I think, in the interests of just practicing on the code-base, I'll
> stick with the ALU FV requirements for the time being. I'm just
> becoming comfortable with spelunking that code. I'd like to feel
> useful for a while before I start another task. :)
well, the ALU pipeline correctness proof is done already, and the Logical
Trap is like the "next least complicated" one, pretty much along the same
lines as SPR.
MUL is more challenging (more involved) as there are sign-swapping, 32 bit,
64 bit, etc involved.
DIV *might* actually be straightforward to do hum except as a FSM it'll
need some timing logic.
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
More information about the libre-riscv-dev