[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 #8 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #5)
> https://www.cl.cam.ac.uk/~jrh13/papers/tang.html
> 
> although quite old and archaic this looks very good,
> there must be more.

yup. unfortunately afaict from reading the first few pages, this paper's basic
idea is "lets use a formal proof program that lets us use real numbers, making
it easier to check if our fp is correct since we can just round those real
numbers to the correct fp answers."

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