[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

Jacob Lifshay <programmerjake at gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|CONFIRMED                   |IN_PROGRESS

--- Comment #13 from Jacob Lifshay <programmerjake at gmail.com> ---
I created a demo f32 fmul round-to-nearest-ties-to-even formal proof in smtlib2
format to see if current solvers are actually have good enough fp support to be
usable.

I tried running it in z3 and it just kept running for 5-10min (after about 15
rounds of fixing bugs in my fmul implementation)...I canceled it for now and
committed my work, I'll try running it longer tomorrow.

https://git.libre-soc.org/?p=ieee754fpu.git;a=commit;h=eb55e2592d0dba8565beff291aeee45bceffe9b8

Author: Jacob Lifshay <programmerjake at gmail.com>
Date:   Fri May 13 01:23:32 2022 -0700

    add fpmul_test.smt2 as a test to see if we should bother trying to wire-up
smtlib2 real and fp support in yosys and nmigen

    It's probably correct, z3 ran longer than I bothered to wait, it usually
stops relatively quickly if there's an error in the logic.

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