[libre-riscv-dev] introduction to Formal Mathematical Proof team

[Jacob Lifshay]

On Tue, Jan 7, 2020, 10:17 Luke Kenneth Casson Leighton <lkcl at lkcl.net>
wrote:

> hi, all,
>
> we have some new people who will be part of the formal mathematical
> proof team, Bartek, Julius and Maciej.  they are all mathematicians,
> and i will leave it to them to introduce themselves.  with thanks to
> my brother dan for helping find them :)
>

Welcome all, glad to have you all help out!

Later, when you're working on the floating-point unit, you might find
simple-soft-float to be useful: it's a reference implementation of the IEEE
754 FP standard that I wrote. It's intended to be easily readable rather
than fast, so it's built on the algebraic-numbers library I wrote
(algebraics) -- hopefully making it easier to understand since you can just
treat it as if it's a real number rather than getting bogged down in the
details of computing using limited-size integers.

https://crates.io/crates/algebraics
https://crates.io/crates/simple-soft-float

Note that simple-soft-float is not complete when emulating non-RISC-V
architectures, where NaN payload propagation is not completely implemented.
It's complete for RISC-V since RISC-V doesn't propagate NaN payloads anyway.

Jacob Lifshay

>