Bug 877

Summary:	implementation and formal correctness proof for fp fused-mul-add pipeline excluding ieee754 exception flags
Product:	Libre-SOC's first SoC	Reporter:	Luke Kenneth Casson Leighton <lkcl>
Component:	Formal Verification	Assignee:	Jacob Lifshay <programmerjake>
Status:	RESOLVED FIXED
Severity:	enhancement	CC:	libre-soc-bugs, programmerjake
Priority:	---
Version:	unspecified
Hardware:	PC
OS:	Linux
See Also:	https://bugs.libre-soc.org/show_bug.cgi?id=874 https://bugs.libre-soc.org/show_bug.cgi?id=48 https://bugs.libre-soc.org/show_bug.cgi?id=123
NLnet milestone:	NLNet.2019.10.032.Formal	total budget (EUR) for completion of task and all subtasks:	1650
budget (EUR) for this task, excluding subtasks' budget:	1650	parent task for budget allocation:	196
child tasks for budget allocation:		The table of payments (in EUR) for this task; TOML format:	[jacob] amount = 1650 submitted = 2022-07-06 paid = 2022-07-21
Bug Depends on:	835
Bug Blocks:	196

Description Luke Kenneth Casson Leighton 2022-07-01 08:40:13 BST

similar to bug #869 a formal correctness proof is needed for
fused-mul-add

* f8 (non-standard -- 5 exponent bits, 2 bits in mantissa field, 3-bit mantissa value):
    * DONE: implement other rounding modes in the fmadd pipeline
    * DONE: implement fmsub, fnmadd, fnmsub
    * DONE: formal verification
* f16:
    * DONE: implement other rounding modes in the fmadd pipeline
    * DONE: implement fmsub, fnmadd, fnmsub
    * REMOVED: formal verification -- didn't complete after >8hr
* f32 (if smt solver can handle it):
    * DONE: implement other rounding modes in the fmadd pipeline
    * DONE: implement fmsub, fnmadd, fnmsub
    * REMOVED: formal verification -- f16 is too slow, didn't attempt f32
* f64 (if smt solver can handle it):
    * DONE: implement other rounding modes in the fmadd pipeline
    * DONE: implement fmsub, fnmadd, fnmsub
    * REMOVED: formal verification -- f16 is too slow, didn't attempt f64

Comment 1 Jacob Lifshay 2022-07-04 12:03:40 BST

I implemented fmadd, fmsub, fnmadd, and fnmsub and now just have to work out the remaining bugs.

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

I probably got fmadd and fnmsub to work for all rounding modes, I'm currently running the formal proofs overnight -- hopefully they won't take too long to run.

fmsub and fnmadd have a bug which I'll debug tomorrow.

Comment 2 Jacob Lifshay 2022-07-04 12:34:48 BST

(In reply to Jacob Lifshay from comment #1)
> fmsub and fnmadd have a bug which I'll debug tomorrow.

i think i found the bug by reading the diff:
i forgot to flip `b`'s sign when `negate_addend` is set in the `0 + x` special case:
https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fpfma/special_cases.py;h=826c32a8e80f2a121a585d7c83bb65e436e97d50;hb=449176c8896dd13ae80130a3a0c8fc88026a2499#l247

i'll fix it tomorrow when it's not 4:30am

Comment 3 Jacob Lifshay 2022-07-05 00:45:01 BST

(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.

Comment 4 Jacob Lifshay 2022-07-05 00:46:31 BST

*** Bug 123 has been marked as a duplicate of this bug. ***