[Libre-soc-bugs] [Bug 196] Formal correctness proof needed for the IEEE754 FPU

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=196

--- Comment #3 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #2)
> https://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf

afaict from reading the first few pages, this particular paper isn't what we
want, since it's focused on formal proofs of C programs based on pre-existing
known-correct fp operations. what we want is instead formal proofs of those fp
operations. that said, its list of references could be useful.
> 
> some interesting leads and papers, it looks like there
> have been quite a few Formal Correctness Proof attempts
> on IEEE754 FP already.

yes.

> which if true would make this more a task of applying
> those rather than attempting to create a new one from
> scratch.

the problem is that all the formal proofs of floating-point that I've seen are
based on comparing the floating-point operation to doing the operation on
infinite-precision real numbers and then rounding that to the correct
floating-point number. The problem is that, because our formal proofs are
written in nmigen, they have to go through yosys translation before getting to
the smtlib2 language (the actual input language for the smt solvers -- which
supports real numbers (actually real algebraic numbers, it lacks transcendental
ops/constants)). yosys doesn't support anything but bitvectors and arrays of
bitvectors -- no real numbers (don't confuse it with yosys's partial support
for verilog reals but only in parameters and only as literal numbers -- verilog
real is a double, not a real number).

> that approach is IMPORTANT because those pre-existing
> Proofs would be a "known-good".
> 
> attempting to reinvent the wheel unnecessarily actually
> introduces the serious risk of not having provenance
> behind the newly-invented Proof.

-- 
You are receiving this mail because:
You are on the CC list for the bug.