[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 #31 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #30)
> the next test then would be to try FP16

I created a fp16 variant:
https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=fp16mul_test.smt2;h=6ad9dc798eb34c72357c3d94d953de01493a5795;hb=c17c88ffba83c546ae439238fdd43adce3992f53

currently running z3 and cvc5, though cvc5's support for stuff other than
f32/f64 is experimental and may be broken.

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