* f16: * DONE: implement other rounding modes in the fadd pipeline * DONE: formal verification of all rounding modes * f32 (if smt solver can handle it): * DONE: implement other rounding modes in the fadd pipeline * DONE: formal verification of all rounding modes * f64 (if smt solver can handle it): * DONE: implement other rounding modes in the fadd pipeline * REMOVED: formal verification of all rounding modes smt solver can't handle it in a reasonably short amount of time, I gave up after 15min, as mentioned in https://bugs.libre-soc.org/show_bug.cgi?id=869#c1 If anyone wants to try running it longer, I expect the formal proof to succeed if the smt solver actually finishes.
I finished implementing and formally proving fadd for f16/f32 and for all rounding modes in the OpenPower spec. https://git.libre-soc.org/?p=ieee754fpu.git;a=commit;h=78bc58e1e6031a81620ced176b798f2e9e4703d1 Copied the same amount of payment as for #869, lkcl let me know if you think that's fine.