Steps: * f16: * DONE: formal verification of fadd for just round-nearest-ties-to-even where NaNs are not distinguished from each other and exception flags/traps aren't checked * DONE: formal verification of correct NaN propagation/generation * f32: * DONE: formal verification of fadd for just round-nearest-ties-to-even where NaNs are not distinguished from each other and exception flags/traps aren't checked * DONE: formal verification of correct NaN propagation/generation * f64 -- determined that running the tests is too slow, but should be done. https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fpadd/test/test_add_formal.py;h=2d3584d26c7f2b9c98ea7d95d0a79b4730cd83dd;hb=HEAD
I implemented correct NaN propagation for the fadd pipeline, so this task is complete. considering that this whole task was only 2 days of work, I think eur 1500 is probably too much, lkcl, I'll let you change it to a more suitable value. I switched to bitwuzla for the smt solver, which made it run *much* faster than z3 for this particular test, fast enough that I can run the f32 formal proof too. on my computer: f16 takes 11s f32 takes 3m15s f64 takes >15m so I set it to be skipped
(In reply to Jacob Lifshay from comment #1) > I implemented correct NaN propagation for the fadd pipeline, so this task is > complete. considering that this whole task was only 2 days of work, I think > eur 1500 is probably too much, no, it really isn't. you find these "easy" but they're extremely challenging, and we lost a contributor two years ago because of underpayment. please don't publicly devalue the work that you're doing. i was quoted around EUR 80,000 for a formal correctness proof of IEEE754FP from an Industry source at market rates.