[libre-riscv-dev] daily kan-ban update 26may2020

[Luke Kenneth Casson Leighton]

On Tue, May 26, 2020 at 5:44 PM Cesar Strauss <cestrauss at gmail.com> wrote:

> * Found out about ongoing formal proof work on the very module to which
> I'm adding unit tests. Interesting subject, formal proofs. I've been
> learning it myself, in order to apply it to my work, but have as yet no
> practical experience.

samuel falvo was the first one to explain the benefits of formal proofs.
http://chiselapp.com/user/kc5tja/repository/kestrel-3/artifact/96ea88450c1a3fc6

the insight that he gave particularly hit home when we had to run
literally hundreds of thousands of tests (which takes about a week to
run) for the IEEE754 FPU...

... and yet, despite that, we *still have no guarantee of hitting all
corner-cases*.

so we have hundreds of thousands of tests - with no guarantee - or, we
write *ONE* formal proof that covers them all.

it's not a difficult choice to make.

> Today:
>
> * Advance on the parallel tests. Hopefully, get good progress on the
> rd/wr protocol.

one step at a time.

l.