[libre-riscv-dev] Using formal to expose bugs in scoreboard

[Luke Kenneth Casson Leighton]

On Mon, Jun 8, 2020 at 4:11 AM Yehowshua <yimmanuel3 at gatech.edu> wrote:
>
> This error highlights the need for formal on the scoreboard.

this exact need was taken into consideration when the application for
NLNet Funding for the Formal Correctnes Proofs was made, a year ago.
https://bugs.libre-soc.org/show_bug.cgi?id=81

as it is critically important a budget of EUR 5,000 was allocated just
to this *one* task:
https://bugs.libre-soc.org/show_bug.cgi?id=197

michael began a Formal Correctness Proof for the MultiCompUnit on the
24th of May:
https://bugs.libre-soc.org/show_bug.cgi?id=342

that Correctness Proof is designed to complement the bugreport that
you referenced (see further below)
https://bugs.libre-soc.org/show_bug.cgi?id=336#c54

Samuel Falvo's work was what originally inspired us to use a hybrid
combination of "simple, clear, well-documented" unit tests plus
extensive Formal Correctness Proofs:
http://lists.libre-riscv.org/pipermail/libre-riscv-dev/2019-August/002311.html

although i cannot find the original discussion, it is elsewhere on the
internet several months prior to the Aug 2019 discussion, Samuel's
insights showed us that writing comprehensive Unit Tests simply does
not catch everything, and even if efforts are made to try to do so the
sheer quantity of code involved masks errors, distracts from the
actual code being tested, and doesn't catch all errors anyway.

the IEEE754 FPU tests are a good example.  this is the basic
infrastructure that allows hundreds of thousands of random and
regression tests to be called:
https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fpcommon/test/case_gen.py;hb=HEAD
https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fpcommon/test/fpmux.py;hb=HEAD

and each pipeline then contains sometimes up to 10 separate unit tests
to cover different aspects:
https://git.libre-soc.org/?p=ieee754fpu.git;a=tree;f=src/ieee754/fpdiv/test;hb=HEAD
https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fpmax/test/test_fpmax_pipe.py;hb=HEAD
https://git.libre-soc.org/?p=ieee754fpu.git;a=tree;f=src/ieee754/fpadd/test;hb=HEAD
https://git.libre-soc.org/?p=ieee754fpu.git;a=tree;f=src/ieee754/fpcmp/test;hb=HEAD

none of which *actually* gives us full confidence in the code, despite
taking a week to run even on the fastest modern machines available.
many of the errors during the 6+ month development of the IEEE754 FPU
code were only caught by running well over 100,000 random tests on the
code when parameterised down to FP16.

with only 65536 possible values in FP16, this gave a high probability
that corner-cases would be caught, and in some cases (single parameter
rather than two 2^16 parameters) allows for full coverage.


therefore, yes: the idea has always been to follow this step-by-step
process, for *all* code:

1) write the code and a basic "understanding" unit test infrastructure
sufficient to get the code functional
2) write Formal Correctness Proofs that catch errors
3) write *SIMPLE* unit tests that in no way cover the entirety of the
code: their purpose is as a *tutorial* and example of how to use the
code.

good examples of (3) when it comes to the pipeline API are here:
https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/test/test_buf_pipe.py;hb=HEAD
https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/test/test_inout_mux_pipe.py;hb=HEAD

l.