[libre-riscv-dev] spr formal proof, NLNet RFPs

[libre-riscv-dev] spr formal proof, NLNet RFPs

[Luke Kenneth Casson Leighton]

samuel: next step is to move the task to "completed"
https://libre-soc.org/Samuel_A_Falvo_II/

given that you're in the U.S., unless you open yourself a Transferwise
online bank account (accepting EUR currency) NLNet have asked us to
submit non-EU Requests for Payment at reasonably large amounts so that
bank fees are not extortionate.  (EU accounts including Transferwise
International online accounts they have zero bank fees)

basically, pick your next proof :)  Trap, MUL, DIV, or ShiftRot
"rotate and clear",
they all need doing.

or if you get bored of that there is a key strategic piece of code that needs
writing: the LDSTSplitter.

l.

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] spr formal proof, NLNet RFPs

[Samuel Falvo II]

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.  :)


On Fri, Jul 17, 2020 at 11:52 AM Luke Kenneth Casson Leighton
<lkcl@lkcl.net> wrote:
>
> samuel: next step is to move the task to "completed"
> https://libre-soc.org/Samuel_A_Falvo_II/
>
> given that you're in the U.S., unless you open yourself a Transferwise
> online bank account (accepting EUR currency) NLNet have asked us to
> submit non-EU Requests for Payment at reasonably large amounts so that
> bank fees are not extortionate.  (EU accounts including Transferwise
> International online accounts they have zero bank fees)
>
> basically, pick your next proof :)  Trap, MUL, DIV, or ShiftRot
> "rotate and clear",
> they all need doing.
>
> or if you get bored of that there is a key strategic piece of code that needs
> writing: the LDSTSplitter.
>
> l.
>
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev@lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev



--
Samuel A. Falvo II

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] spr formal proof, NLNet RFPs

[Luke Kenneth Casson Leighton]

On Friday, July 17, 2020, Samuel Falvo II <sam.falvo@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
one.

Trap is like the "next least complicated" one, pretty much along the same
lines as SPR.

https://bugs.libre-soc.org/show_bug.cgi?id=421

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.

l.



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev