[Libre-soc-bugs] [Bug 877] implementation and formal correctness proof for fp fused-mul-add pipeline excluding ieee754 exception flags

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=877

Jacob Lifshay <programmerjake at gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|IN_PROGRESS                 |RESOLVED
         Resolution|---                         |FIXED

--- Comment #3 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Jacob Lifshay from comment #2)
> (In reply to Jacob Lifshay from comment #1)
> > fmsub and fnmadd have a bug which I'll debug tomorrow.

I fixed the bug.

Since the formal proofs for f16 fma didn't finish after >8hr, I disabled f16
formal proofs by default and added f8 formal proofs:
I added support for non-standard floating-point types so we can test f8 (eb=5,
sb=3), all those passed without issue.

https://git.libre-soc.org/?p=ieee754fpu.git;a=commit;h=a434759860b4e6a92c4c46d4842e767ae5b680e3

I also finished cleaning up all the remaining fixmes, and optimized the amount
of padding needed in the intermediate sum.

https://git.libre-soc.org/?p=ieee754fpu.git;a=commit;h=80f6d6471d627c1af572d37b99643c66bbe8be67

I'm considering this completed.

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