[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 mailing list