[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 #23 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
21 seconds.

    $z3 -version
    Z3 version 4.8.5 - 64 bit



lkcl at fizzy:~/src/libresoc/ieee754fpu$ time z3 -smt2 fpmul_test.smt2 
should return unsat:
sat
dumping values in case it returned sat:
((a #x80000000)
 (b #xff800000)
 (p #x7f800002)
 ((f32_to_fp a) (_ -zero 8 24))
 ((f32_to_fp b) (_ -oo 8 24))
 ((fp.mul RNE (f32_to_fp a) (f32_to_fp b)) (_ NaN 8 24))
 ((f32_to_fp (f32_mul_rne a b)) (_ +oo 8 24))
 ((f32_mul_nonzero_finite_rne a b) #x40800000)
 ((f32_mantissa_field a) #b00000000000000000000000)
 ((f32_mantissa_value a) #x800000)
 ((f32_mantissa_field b) #b00000000000000000000000)
 ((f32_mantissa_value b) #x800000)
 (product #x400000000000)
 (sign #b0)
 (exponent #x002)
 ((bv48_clz product) #x000000000001)
 ((ite (bvult #x00000000FFFF product) #x000000000000 #x000000000010)
#x000000000000)
 (norm_product #x800000000000)
 (norm_exponent #x002)
 (subnormal_shift #xf80)
 (product_subnormal #x000000000001)
 (half_way_subnormal false)
 (is_even_subnormal true)
 (rounded_up_subnormal #x000000800001)
 (round_up_overflows_subnormal false)
 (do_round_up_subnormal false)
 (exponent_field_normal #x81)
 (half_way_normal false)
 (is_even_normal true)
 (rounded_up_normal #x800000800000)
 (round_up_overflows_normal false)
 (do_round_up_normal false))

real    0m21.179s
user    0m21.147s
sys     0m0.024s

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