[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 #30 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Jacob Lifshay from comment #29)

> I ran both z3 and cvc5, I stopped both of them after 3hr...that's definitely
> too slow to be readily useful.

still running here (overnight).

so.

there is not yet a sense of "scale", i.e. this is still "unknown".

to get a sense of scale of time, a "success" must be achieved.

the next test then would be to try FP16, BF16, or even FP8.
FP8 would be so tiny (assume 4-bit exponent, 3-bit mantissa)
that it should complete even brute-force.

comparing then to FP16 and then BF16 should give a sense of
whether the scale of completion time is exponential or other.

it does not matter - at all - that brute-force "might be better"
it also does not strictly matter that the ultimate desire is to
prove FP32 and FP64: given that the FP classes are parameterised
and it is identical code i would say that if the FP classes
*in general* succeed at lower bitwidths that there is a reasonable
chance they are correct at the larger.

[this is not entirely true due to the number of pipeline/FSM
 stages varying, but their chain and sequence does not vary]

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