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

[Luke Kenneth Casson Leighton]

On 1/7/20, Jacob Lifshay <programmerjake at gmail.com> wrote:

> Welcome all, glad to have you all help out!

thank you for this, jacob.

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

in talking with bartok off-list, he did describe an algorithmic
(recursive) formal proof concept, which would be nice to see the
details of, here.  it involved each stage providing an algorithmic
representation of FP numbers and then proving that the error is less
than a set bounds, on each iteration.

however it was based on the assumption that we're using Newton Raphson
(which we're not), it's a pipelined design based on variations around
"long division".  could be adapted, fine.

l.