[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 #32 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Jacob Lifshay from comment #31)
> (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.

success on both z3 and cvc5!

log-cvc5.txt:fp16mul_test.smt2:12.12: No set-logic command was given before
this point.
log-cvc5.txt:fp16mul_test.smt2:12.12: cvc5 will make all theories available.
log-cvc5.txt:fp16mul_test.smt2:12.12: Consider setting a stricter logic for
(likely) better performance.
log-cvc5.txt:fp16mul_test.smt2:12.12: To suppress this warning in the future
use (set-logic ALL).
log-cvc5.txt:"should return unsat:"
log-cvc5.txt:unsat
log-cvc5.txt:"dumping values in case it returned sat:"
log-cvc5.txt:(error "Cannot get value unless after a SAT or UNKNOWN response.")
log-cvc5.txt:
log-cvc5.txt:real       106m35.297s
log-cvc5.txt:user       106m31.478s
log-cvc5.txt:sys        0m0.916s
log-z3.txt:should return unsat:
log-z3.txt:unsat
log-z3.txt:dumping values in case it returned sat:
log-z3.txt:(error "line 410 column 1: model is not available")
log-z3.txt:
log-z3.txt:real 77m36.487s
log-z3.txt:user 77m35.130s
log-z3.txt:sys  0m0.236s

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