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

Luke Kenneth Casson Leighton lkcl at lkcl.net
Tue May 26 18:07:14 BST 2020

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.

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

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.


More information about the libre-riscv-dev mailing list